shatters_iff — Mathlib

English

For a finite α, a family 𝒜 shatters s if and only if the image of 𝒜 under the map t ↦ s ∩ t equals the power set of s.

Русский

Для конечного множества α: 𝒜 шаттерит s тогда и только тогда, когда образ 𝒜 при отображении t ↦ s ∩ t совпадает с множестом подмножеств s.

LaTeX

$$$\\mathcal{A}.Shatters s \\iff \\mathrm{image}(\\lambda t. s\\cap t)\\, \\mathcal{A} = s\\text{ powerset}$$$

Lean4

theorem shatters_iff : 𝒜.Shatters s ↔ 𝒜.image (fun t ↦ s ∩ t) = s.powerset :=
  ⟨fun h ↦ by ext t; rw [mem_image, mem_powerset, h.subset_iff], fun h t ht ↦ by
    rwa [← mem_powerset, ← h, mem_image] at ht⟩

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