English
Let f be monotone and φ: ι₁ → ι₂ converge to atTop. Then Tendsto f atTop to l iff Tendsto f∘φ atTop to l.
Русский
Пусть f монотонна и φ достигает atTop. Тогда Tendsto f atTop to l эквівалентно Tendsto (f∘φ) atTop to l.
LaTeX
$$$ \text{Monotone}(f) \Rightarrow \bigl( \operatorname{Tendsto}\! \phi \!\operatorname{atTop} \operatorname{atTop} \Rightarrow
\left( \operatorname{Tendsto} f \operatorname{atTop} (\nhds l) \iff \operatorname{Tendsto} (f \circ \phi) \operatorname{atTop} (\nhds l) \right) \Bigr)$$$
Lean4
theorem tendsto_iff_tendsto_subseq_of_monotone {ι₁ ι₂ α : Type*} [SemilatticeSup ι₁] [Preorder ι₂] [Nonempty ι₁]
[TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [NoMaxOrder α] {f : ι₂ → α}
{φ : ι₁ → ι₂} {l : α} (hf : Monotone f) (hg : Tendsto φ atTop atTop) :
Tendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l) :=
by
constructor <;> intro h
· exact h.comp hg
· rcases tendsto_of_monotone hf with (h' | ⟨l', hl'⟩)
· exact (not_tendsto_atTop_of_tendsto_nhds h (h'.comp hg)).elim
· rwa [tendsto_nhds_unique h (hl'.comp hg)]
