English
Let s: β → Set γ be monotone and g: α → β tend to atBot along a nontrivial filter l. Then the indexed intersection of s ∘ g equals the intersection of s over β; i.e., ⋂_a s(g(a)) = ⋂_b s(b).
Русский
Пусть s: β → Set γ монотонна и g: α → β стремится к нижней границе вдоль ненулевого фильтра l. Тогда индексированное пересечение s ∘ g равно пересечению по β; то есть ⋂_a s(g(a)) = ⋂_b s(b).
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 intersection of `s ∘ f` is equal to the indexed intersection of `s`. -/
theorem _root_.Monotone.iInter_comp_tendsto_atBot [Preorder β] {l : Filter α} [l.NeBot] {s : β → Set γ}
(hs : Monotone s) {f : α → β} (hf : Tendsto f l atBot) : ⋂ a, s (f a) = ⋂ b, s b :=
hs.iInf_comp_tendsto_atBot hf
