English
A set family 𝒜 shatters a set s if every subset t of s can be written as the intersection s ∩ u for some u ∈ 𝒜. We call s traced by 𝒜 in that case.
Русский
Семейство множеств 𝒜 шатрирует множество s, если каждое подмножество t ⊆ s может быть записано как s ∩ u для некоторого u ∈ 𝒜. Тогда говорят, что s прослеживается 𝒜.
LaTeX
$$Def: 𝒜.Shatters s : ∀ t ⊆ s, ∃ u ∈ 𝒜, s ∩ u = t$$
Lean4
/-- A set family `𝒜` shatters a set `s` if all subsets of `s` can be obtained as the intersection
of `s` and some element of the set family, and we denote this `𝒜.Shatters s`. We also say that `s`
is *traced* by `𝒜`. -/
def Shatters (𝒜 : Finset (Finset α)) (s : Finset α) : Prop :=
∀ ⦃t⦄, t ⊆ s → ∃ u ∈ 𝒜, s ∩ u = t
