shatterer_eq — Mathlib

English

The shatterer of 𝒜 equals 𝒜 if and only if 𝒜 is a lower set.

Русский

Shatterer(𝒜) = 𝒜 тогда и только тогда, когда 𝒜—нижнее множество.

LaTeX

$$$𝒜.shatterer = 𝒜 \\iff IsLowerSet (𝒜 : Set (Finset α))$$$

Lean4

@[simp]
theorem shatterer_eq : 𝒜.shatterer = 𝒜 ↔ IsLowerSet (𝒜 : Set (Finset α)) :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ Subset.antisymm (fun s hs ↦ ?_) <| subset_shatterer h⟩
  · rw [← h]
    exact isLowerSet_shatterer _
  · obtain ⟨t, ht, hst⟩ := (mem_shatterer.1 hs).exists_superset
    exact h hst ht

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