biInter_le

Mathlib.Data.Set.Lattice

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

English

For a PartialOrder ι and s : ι → Set α, the intersection over j ≤ i of s_j equals the intersection over j < i of s_j intersected with s_i.

Русский

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

LaTeX

$$$$ \bigcap_{j \le i} s(j) = \bigcap_{j < i} s(j) \cap s(i) $$$$

Lean4

theorem biInter_le : (⋂ j ≤ i, s j) = (⋂ j < i, s j) ∩ s i :=
  biInf_le_eq_inf s i

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

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

Разделы

Аффилиация

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