tendsto_one_iff_mabs_tendsto_one — Mathlib

English

For any f, Tendsto f to 1 iff Tendsto mabs ∘ f to 1.

Русский

Для любой функции f: Tendsto f к 1 эквивалентно Tendsto |f| к 1.

LaTeX

$$$\mathrm{Tendsto}\ f\ l\to (\mathcal{nhds}\ 1) \iff \mathrm{Tendsto}\ (\mathrm{mabs}\circ f)\ l\to (\mathcal{nhds}\ 1).$$$

Lean4

@[to_additive]
theorem tendsto_one_iff_mabs_tendsto_one (f : α → G) : Tendsto f l (𝓝 1) ↔ Tendsto (mabs ∘ f) l (𝓝 1) := by
  rw [← tendsto_comap_iff, comap_mabs_nhds_one]

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