tendsto_atBot_mul_const_right — Mathlib

English

In a group with order, multiplying by a fixed element C on the right preserves Tendsto toTop if f tends to top; a symmetric statement holds for left multiplication with the corresponding dual order.

Русский

В группе с порядком умножение на фиксированный элемент C справа сохраняет стремление к верху, если функция f стремится к верху; симметричное утверждение верно и слева с соответствующей двойственной структурой.

LaTeX

$$$\\forall l:\\Filter\\ α,\\ \\forall f:\\alpha\\to G,\\ \\mathrm{Tendsto} f\\ l\\ atTop\\Rightarrow \\mathrm{Tendsto}(f\\cdot C)\\ l\\ atTop$$$

Lean4

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

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