biInter_lt_eq_iInter

Mathlib.Data.Set.Lattice

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

English

The set pi i s equals the intersection over a ∈ i of the preimage of s a under eval a.

Русский

Множество pi i s равно пересечению по a ∈ i предобраза s(a) через eval a.

LaTeX

$$$$ \pi i s = \bigcap_{a \in i} \operatorname{eval}_a^{-1}(s(a)) $$$$

Lean4

theorem biInter_lt_eq_iInter [LT α] [NoMaxOrder α] {s : α → Set β} : ⋂ (n) (m < n), s m = ⋂ (n), s n :=
  biInf_lt_eq_iInf

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

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

Разделы

Аффилиация

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