conformalAt_const_smul — Mathlib

English

For a nonzero scalar c, the map x ↦ c x is conformal at every x.

Русский

Для ненулевого скаляра c отображение x ↦ c x конформно в любой точке.

LaTeX

$$$\\operatorname{ConformalAt}(\\lambda x. c \\cdot x, x)$ for any x and $c \\neq 0$$$

Lean4

theorem conformalAt_const_smul {c : ℝ} (h : c ≠ 0) (x : X) : ConformalAt (fun x' : X => c • x') x :=
  ⟨c • ContinuousLinearMap.id ℝ X, (hasFDerivAt_id x).const_smul c, isConformalMap_const_smul h⟩

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