English
Let s: β → Set γ be monotone and f: α → β tend to atTop along a nontrivial filter l. Then the indexed union of the sets s(f(a)) equals the union over all β; i.e., ⋃_a s(f(a)) = ⋃_b s(b).
Русский
Пусть s: β → Set γ монотонна и f: α → β стремится к верхней границе вдоль ненулевого фильтра l. Тогда индексированное объединение множеств s(f(a)) равно объединению всех s(b) по b; то есть ⋃_a s(f(a)) = ⋃_b s(b).
LaTeX
$$$$\bigcup_{a} s(f(a)) = \bigcup_{b\in\beta} s(b).$$$$
Lean4
/-- If `s` is a monotone family of sets and `f` tends to `atTop` along a nontrivial filter,
then the indexed union of `s ∘ f` is equal to the indexed union of `s`. -/
theorem _root_.Monotone.iUnion_comp_tendsto_atTop [Preorder β] {l : Filter α} [l.NeBot] {s : β → Set γ}
(hs : Monotone s) {f : α → β} (hf : Tendsto f l atTop) : ⋃ a, s (f a) = ⋃ b, s b :=
hs.iSup_comp_tendsto_atTop hf
