biInter_gt_eq_iInf — Mathlib

English

Let α be a type with LT and NoMinOrder. Then 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 > n} s(m) = \bigcap_{n} s(n) $$$$

Lean4

theorem biInter_gt_eq_iInf [LT α] [NoMinOrder α] {s : α → Set β} : ⋂ (n) (m > n), s m = ⋂ n, s n :=
  biInf_gt_eq_iInf

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