tendsto_atTop_atTop_iff_of_monotone

English

If f is monotone, Tendsto f atTop to atTop is equivalent to: for every b there exists a with b ≤ f(a).

Русский

Если f монотонна, тогда сходимость f от atTop к atTop эквивалентна: для каждого b существует a, такой что b ≤ f(a).

LaTeX

$$$\forall\!{f},\ (Monotone\ f) \rightarrow (Tendsto\ f\ atTop\ atTop \leftrightarrow \forall b, \exists a, b \le f(a))$$$

Lean4

theorem tendsto_atTop_atTop_iff_of_monotone (hf : Monotone f) : Tendsto f atTop atTop ↔ ∀ b : β, ∃ a, b ≤ f a :=
  tendsto_atTop_atTop.trans <|
    forall_congr' fun _ => exists_congr fun a => ⟨fun h => h a (le_refl a), fun h _a' ha' => le_trans h <| hf ha'⟩

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