IsConformalMap — Mathlib

English

If f is conformal, multiplying by a nonzero scalar preserves conformality.

Русский

Если f конформно, умножение на ненулевой скаляр сохраняет конформность.

LaTeX

$$$\\mathrm{IsConformalMap}(f) \\rightarrow \\forall c \\neq 0, \\mathrm{IsConformalMap}(f \\cdot c)$$$

Lean4

/-- A continuous linear map `f'` is said to be conformal if it's
a nonzero multiple of a linear isometry. -/
def IsConformalMap {R : Type*} {X Y : Type*} [NormedField R] [SeminormedAddCommGroup X] [SeminormedAddCommGroup Y]
    [NormedSpace R X] [NormedSpace R Y] (f' : X →L[R] Y) :=
  ∃ c ≠ (0 : R), ∃ li : X →ₗᵢ[R] Y, f' = c • li.toContinuousLinearMap

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