biUnion_gt_eq_iUnion — Mathlib

English

For α with LT and NoMinOrder, the union over n of the unions over m > n of s(m) equals the union over n of s(n).

Русский

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

LaTeX

$$$$ \bigcup_{n} \bigcup_{m > n} s(m) = \bigcup_{n} s(n) $$$$

Lean4

theorem biUnion_gt_eq_iUnion [LT α] [NoMinOrder α] {s : α → Set β} : ⋃ (n) (m > n), s m = ⋃ n, s n :=
  biSup_gt_eq_iSup

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