countable_iInter_mem

Mathlib.Order.Filter.CountableInter

URI: https://scilib.ai/kg/mathlib#countable_iInter_mem

← MathLib Explorer

English

If ι is countable, then ∩_{i} s_i ∈ l iff ∀ i, s_i ∈ l.

Русский

Если ι счетно, то ∩ s_i ∈ l тогда и только тогда, когда каждый s_i ∈ l.

LaTeX

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

Lean4

theorem countable_iInter_mem [Countable ι] {s : ι → Set α} : (⋂ i, s i) ∈ l ↔ ∀ i, s i ∈ l :=
  sInter_range s ▸ (countable_sInter_mem (countable_range _)).trans forall_mem_range

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru