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'