subset_shatterer — Mathlib

English

If 𝒜 is a lower set in the subset order, then every element of 𝒜 belongs to the shatterer of 𝒜.

Русский

Если 𝒜 образует нижнее множество по отношению подмножества, то каждое его элемент принадлежит к 𝒜.shatterer.

LaTeX

$$$IsLowerSet(\\mathcal{A}) \\Rightarrow \\mathcal{A} \\subseteq 𝒜.shatterer$$$

Lean4

theorem subset_shatterer (h : IsLowerSet (𝒜 : Set (Finset α))) : 𝒜 ⊆ 𝒜.shatterer := fun _s hs ↦
  mem_shatterer.2 fun t ht ↦ ⟨t, h ht hs, inter_eq_right.2 ht⟩

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