tendsto_atBot_atBot_iff_of_monotone

English

If f is monotone, then Tendsto f atBot atBot is equivalent to: for every b in β there exists an a in α such that f(a) ≤ b.

Русский

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

LaTeX

$$$\mathrm{Monotone}(f) \;\Rightarrow\; \mathrm{Tendsto}\ f\ atBot\ atBot \iff \forall b:\beta, \exists a:\alpha, f(a) \le b$$$

Lean4

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

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