memberSubfamily — Mathlib

English

If 𝒜 is downward closed, then the subfamily of those members that contain a fixed a is downward closed as well.

Русский

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

LaTeX

$$$$\\text{If } 𝒜\\text{ is downward closed, then } 𝒜_{\\ni a} \\text{ is downward closed.}$$$$

Lean4

theorem memberSubfamily (h : IsLowerSet (𝒜 : Set (Finset α))) : IsLowerSet (𝒜.memberSubfamily a : Set (Finset α)) :=
  by
  rintro s t hts
  simp_rw [mem_coe, mem_memberSubfamily]
  exact And.imp (h <| insert_subset_insert _ hts) (mt <| @hts _)

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