Shattering

Conjectura.Defs.ComputerScience.Learning.Shatters

/-
Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Samuel Schlesinger
-/
import Conjectura.Defs.ComputerScience.Learning.ConceptClass

/-! # Shattering

## Source

Adapted for Conjectura from [cslib](https://github.com/leanprover/cslib), split into one concept per module. Released by its authors under Apache 2.0.
-/

namespace Conjectura.Learning

/-- A binary concept class **shatters** a set when every one of its subsets is cut out by some
concept — the class can realise every possible labelling of those points. -/
def Shatters {α : Type*} (C : ConceptClass α Bool) (W : Set α) : Prop :=
  ∀ W' ⊆ W, ∃ c ∈ C, ∀ x ∈ W, (c x = true ↔ x ∈ W')

end Conjectura.Learning