conformalAt_iff_isConformalMap_fderiv

English

A map f is conformal at x if and only if its derivative at x is a conformal linear map.

Русский

Отображение конформно в x тогда и только тогда, когда производная f в x является конформным линейным отображением.

LaTeX

$$$\\operatorname{ConformalAt}(f,x) \\iff \\operatorname{IsConformalMap}(fderiv_\\mathbb{R} f x)$$$

Lean4

/-- A function is a conformal map if and only if its differential is a conformal linear map -/
theorem conformalAt_iff_isConformalMap_fderiv {f : X → Y} {x : X} : ConformalAt f x ↔ IsConformalMap (fderiv ℝ f x) :=
  by
  constructor
  · rintro ⟨f', hf, hf'⟩
    rwa [hf.fderiv]
  · intro H
    by_cases h : DifferentiableAt ℝ f x
    · exact ⟨fderiv ℝ f x, h.hasFDerivAt, H⟩
    · nontriviality X
      exact absurd (fderiv_zero_of_not_differentiableAt h) H.ne_zero

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