biInter_le_eq_iInter — Mathlib

English

For a family s: α → Set β with LT structure on α and NoMaxOrder, the intersection over n of the intersections over m < n equals the intersection over n of s(n).

Русский

Пусть α имеет линейный порядок без максимального элемента; тогда ⋂_n ⋂_{m<n} s(m) = ⋂_n s(n).

LaTeX

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

Lean4

theorem biInter_le_eq_iInter [Preorder α] {s : α → Set β} : ⋂ (n) (m ≤ n), s m = ⋂ (n), s n :=
  biInf_le_eq_iInf

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