nonMemberSubfamily — Mathlib

English

If a family 𝒜 of finite sets is downward closed under inclusion, then the subfamily of 𝒜 consisting of sets not containing a fixed element a is also downward closed.

Русский

Если семейство 𝒜 конечных множеств замкнуто снизу по включению, то подсемейство 𝒜, состоящее из множеств, не содержащих фиксированного элемента a, также замкну снизу.

LaTeX

$$$$\\text{If } 𝒜\\subseteq \\mathcal{P}(X) \\text{ is downward closed, then } 𝒜_{\\setminus a} \\subseteq \\mathcal{P}(X) \\text{ is downward closed.}$$$$

Lean4

theorem nonMemberSubfamily (h : IsLowerSet (𝒜 : Set (Finset α))) :
    IsLowerSet (𝒜.nonMemberSubfamily a : Set (Finset α)) := fun s t hts =>
  by
  simp_rw [mem_coe, mem_nonMemberSubfamily]
  exact And.imp (h hts) (mt <| @hts _)

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