shatterer — Mathlib

English

The shatterer of 𝒜 is the subfamily of all s in the biUnion of 𝒜 with the powerset that are shattered by 𝒜.

Русский

Shatterer(𝒜) — это подсемейство тех $s \in 𝒜 \uplus \mathcal{P}(\alpha)$, которые расшатаны 𝒜.

LaTeX

$$$\\operatorname{shatterer}(\\mathcal{A}) = \\{ s \\in \\mathcal{A}.biUnion(\\mathcal{P}) \\mid \\mathcal{A}.Shatters s \\}$$$

Lean4

/-- The set family of sets that are shattered by `𝒜`. -/
def shatterer (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
  {s ∈ 𝒜.biUnion powerset | 𝒜.Shatters s}

Похожие утверждения