iInter_comp_tendsto_atTop — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If `s` is an antitone family of sets and `f` tends to `atTop` along a nontrivial filter,
then the indexed intersection of `s ∘ f` is equal to the indexed intersection of `s`. -/
theorem _root_.Antitone.iInter_comp_tendsto_atTop [Preorder β] {l : Filter α} [l.NeBot] {s : β → Set γ}
    (hs : Antitone s) {f : α → β} (hf : Tendsto f l atTop) : ⋂ a, s (f a) = ⋂ b, s b :=
  hs.iInf_comp_tendsto_atTop hf

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