iUnion_comp_tendsto_atBot — Mathlib

English

Let s: β → Set γ be antitone and g: α → β tend to atTop along a nontrivial filter l. Then the indexed intersection equals the universal intersection, i.e., ⋂_a s(g(a)) = ⋂_b s(b).

Русский

Пусть s: β → Set γ антимонотна и g: α → β стремится к верхней границе вдоль ненулевого фильтра l. Тогда пересечение по a равно пересечению по β.

LaTeX

$$$$\bigcap_{a} s(g(a)) = \bigcap_{b\in\beta} s(b).$$$$

Lean4

/-- If `s` is a monotone family of sets and `f` tends to `atBot` along a nontrivial filter,
then the indexed union of `s ∘ f` is equal to the indexed union of `s`. -/
theorem _root_.Antitone.iUnion_comp_tendsto_atBot [Preorder β] {l : Filter α} [l.NeBot] {s : β → Set γ}
    (hs : Antitone s) {f : α → β} (hf : Tendsto f l atBot) : ⋃ a, s (f a) = ⋃ b, s b :=
  hs.iSup_comp_tendsto_atBot hf

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