biInter_ge

Mathlib.Data.Set.Lattice

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

English

For a PartialOrder ι, the intersection over j ≥ i of s(j) equals s(i) intersected with the intersection over j > i of s(j).

Русский

Для частичного порядка ι: ⋂_{j ≥ i} s(j) = s(i) ∩ ⋂_{j > i} s(j).

LaTeX

$$$$ \bigcap_{j \ge i} s(j) = s(i) \cap \bigcap_{j > i} s(j) $$$$

Lean4

theorem biInter_ge : (⋂ j ≥ i, s j) = s i ∩ ⋂ j > i, s j :=
  biInf_ge_eq_inf s i

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

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

Разделы

Аффилиация

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