memberSubfamily_subset_nonMemberSubfamily

English

For a downward-closed family, every member Subfamily is contained in the corresponding nonMemberSubfamily (i.e., containing no a) in terms of set inclusion relations.

Русский

Для нисходящего семейства каждый элемент подсемейства содержится в соответствующем подмножестве без элемента a.

LaTeX

$$$$\\mathcal{A}.(a) \\subseteq \\mathcal{A}.\\text{(not }a)$$$$

Lean4

theorem memberSubfamily_subset_nonMemberSubfamily (h : IsLowerSet (𝒜 : Set (Finset α))) :
    𝒜.memberSubfamily a ⊆ 𝒜.nonMemberSubfamily a := fun s =>
  by
  rw [mem_memberSubfamily, mem_nonMemberSubfamily]
  exact And.imp_left (h <| subset_insert _ _)

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