tendsto_mabs_nhdsNE_one — Mathlib

English

The absolute value map has a controlled approach to 1 from the punctured neighborhood of 1, approaching values > 1 along paths approaching 1 from outside 1.

Русский

Мапа мabs имеет управляемое приближение к единице из окрестности единицы без самой единицы, стремясь к значениям > 1 при подходе к единице извне.

LaTeX

$$$\mathrm{Tendsto}\bigl( \mathrm{mabs} : G \to G \bigr)\big( \mathcal{N}_{1}^{\setminus\{1\}} \bigr) \big( \mathcal{N}_{1}^{>1} \bigr).$$$

Lean4

@[to_additive]
theorem tendsto_mabs_nhdsNE_one : Tendsto (mabs : G → G) (𝓝[≠] 1) (𝓝[>] 1) :=
  (continuous_mabs.tendsto' (1 : G) 1 mabs_one).inf <| tendsto_principal_principal.2 fun _x => one_lt_mabs.2

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