cardinal_sInter_mem — Mathlib

English

If S is a family of sets with cardinality less than c and l is a CardinalInterFilter l c, then ⋂₀ S ∈ l iff every s ∈ S belongs to l.

Русский

Если S — семейство множеств с кардиналом меньше c, и l — фильтр CardinalInterFilter l c, то ⋂₀ S ∈ l тогда и только тогда, когда каждый s ∈ S принадлежит l.

LaTeX

$$$$ \\bigcap S \\in l \\iff \\forall s \\in S, s \\in l $$$$

Lean4

theorem cardinal_sInter_mem {S : Set (Set α)} [CardinalInterFilter l c] (hSc : #S < c) : ⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l :=
  ⟨fun hS _s hs => mem_of_superset hS (sInter_subset_of_mem hs), CardinalInterFilter.cardinal_sInter_mem _ hSc⟩

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