countable_sInter_mem — Mathlib

English

Let l be a filter with CountableInterFilter, and l Countable ι. Then for S countable, the intersection ∩_{i∈ι} s_i is in l iff each s_i ∈ l.

Русский

Пусть l — фильтр с CountableInterFilter, и ι — счетно. Тогда пересечение по i ∈ ι принадлежит l тогда и только тогда, когда каждый s_i ∈ l.

LaTeX

$$$\\bigcap_{i} s_i ∈ l \\iff \\forall i, s_i ∈ l$$$

Lean4

theorem countable_sInter_mem {S : Set (Set α)} (hSc : S.Countable) : ⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l :=
  ⟨fun hS _s hs => mem_of_superset hS (sInter_subset_of_mem hs), CountableInterFilter.countable_sInter_mem _ hSc⟩

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