ConformalAt — Mathlib

English

A map f is conformal at a point x if there exists a differential f' : X →L[ℝ] Y such that f has derivative f' at x and f' is conformal.

Русский

Отображение f конформно в точке x, если существует конформный дифференциал f' : X →L[ℝ] Y, и f имеет производную f' в x.

LaTeX

$$$\\exists f' : X \\to_L[\\mathbb{R}] Y,\\ HasFDerivAt\\ f\\ f'\\ x \\wedge IsConformalMap f'$$

Lean4

/-- A map `f` is said to be conformal if it has a conformal differential `f'`. -/
def ConformalAt (f : X → Y) (x : X) :=
  ∃ f' : X →L[ℝ] Y, HasFDerivAt f f' x ∧ IsConformalMap f'

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