cardinal_iInter_mem — Mathlib

English

Let S ⊆ ι with #ι < c, and s : ∀ i ∈ S, Set α. Then (⋂ i, i ∈ S → s i) ∈ l if and only if ∀ i, ∀ hi ∈ i ∈ S, s i hi ∈ l.

Русский

Пусть S ⊆ ι и #ι < c, а функция s задаёт множество для каждого i ∈ S. Тогда ⋂ i∈S s(i) ∈ l тогда и только если для каждого i ∈ S и для каждого hi ∈ i, s(i, hi) ∈ l.

LaTeX

$$$#ι < c \\rightarrow (\\bigcap_{i} s_i) \\in l \\iff \\forall i, s_i \\in l$$$

Lean4

theorem cardinal_iInter_mem {s : ι → Set α} (hic : #ι < c) : (⋂ i, s i) ∈ l ↔ ∀ i, s i ∈ l :=
  by
  rw [← sInter_range _]
  apply (cardinal_sInter_mem (lt_of_le_of_lt Cardinal.mk_range_le hic)).trans
  exact forall_mem_range

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