biInter_ge_eq_iInf

Mathlib.Data.Set.Lattice

URI: https://scilib.ai/kg/mathlib#Set.biInter_ge_eq_iInf

English

For a Preorder α, the intersection over n of the intersections over m ≥ n equals the intersection over n.

Русский

Для Предпорядка α: ⋂_n ⋂_{m≥n} s(m) = ⋂_n s(n).

LaTeX

$$$$ \bigcap_{n} \bigcap_{m \ge n} s(m) = \bigcap_{n} s(n) $$$$

Lean4

theorem biInter_ge_eq_iInf [Preorder α] {s : α → Set β} : ⋂ (n) (m ≥ n), s m = ⋂ n, s n :=
  biInf_ge_eq_iInf

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

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

Разделы

Аффилиация

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