tendsto_atBot_mul_const_left — Mathlib

English

In an ordered group, the inversion map sends atBot to atTop and atTop to atBot; equivalently, Tendsto inv l atBot ↔ Tendsto id l atTop in the appropriate dual sense.

Русский

В упорядоченной группе инверсия переводит нижний предел в верхний и наоборот; эквивалентно, Tendsto inv l atBot ↔ Tendsto id l atTop в соответствующем двойственном виде.

LaTeX

$$$\\mathrm{Tendsto}(\\mathrm{Inv.inv})\\ l\\ (\\mathrm{atBot}\\Rightarrow \\mathrm{atTop})$$$

Lean4

@[to_additive]
theorem tendsto_atBot_mul_const_left (C : G) (hf : Tendsto f l atBot) : Tendsto (fun x => C * f x) l atBot :=
  tendsto_atTop_mul_const_left (G := Gᵒᵈ) _ C hf

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