English
Let f be antitone 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{Antitone}(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_antitone {ι₁ ι₂ α : Type*} [SemilatticeSup ι₁] [Preorder ι₂] [Nonempty ι₁]
[TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [NoMinOrder α] {f : ι₂ → α}
{φ : ι₁ → ι₂} {l : α} (hf : Antitone f) (hg : Tendsto φ atTop atTop) :
Tendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l) :=
tendsto_iff_tendsto_subseq_of_monotone (α := αᵒᵈ) hf hg
