countable_bInter_mem — Mathlib

English

For a countable index set S, the big intersection over i ∈ S with a preceding condition is in l iff every component is in l.

Русский

Для счетного множества индексов S, пересечение по i ∈ S с заданным условием принадлежит l тогда, когда каждый элемент удовлетворяет условию.

LaTeX

$$$(\\bigcap i\\in S, s_i) \\in l \\iff \\forall i, s_i ∈ l$$$

Lean4

theorem countable_bInter_mem {ι : Type*} {S : Set ι} (hS : S.Countable) {s : ∀ i ∈ S, Set α} :
    (⋂ i, ⋂ hi : i ∈ S, s i ‹_›) ∈ l ↔ ∀ i, ∀ hi : i ∈ S, s i ‹_› ∈ l :=
  by
  rw [biInter_eq_iInter]
  haveI := hS.toEncodable
  exact countable_iInter_mem.trans Subtype.forall

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