subset_iff — Mathlib

English

If s is shattered by 𝒜, then t is a subset of s if and only if there exists u in 𝒜 with s ∩ u = t.

Русский

Если s раскатано (шаттерится) 𝒜, то для любого t ⊆ s существует u ∈ 𝒜 such that s ∩ u = t

LaTeX

$$$\\mathcal{A}.Shatters s \\Rightarrow (t \\subseteq s \\iff \\exists u \\in \\mathcal{A}, s \\cap u = t)$$$

Lean4

protected theorem subset_iff (h : 𝒜.Shatters s) : t ⊆ s ↔ ∃ u ∈ 𝒜, s ∩ u = t :=
  ⟨fun ht ↦ h ht, by rintro ⟨u, _, rfl⟩; exact inter_subset_left⟩

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