English
A real differentiable map f is conformal at x iff its differential scales every inner product by a positive scalar.
Русский
Действительно гладкое отображение f конформно в точке x тогда и только тогда, когда дифференциал масштабирует скалярно все скалярные произведения на положительное число.
LaTeX
$$$ \exists c>0, \forall u,v, \langle f'(x)u, f'(x)v \rangle = c \langle u,v \rangle $$$
Lean4
/-- A real differentiable map `f` is conformal at point `x` if and only if its
differential `fderiv ℝ f x` at that point scales every inner product by a positive scalar. -/
theorem conformalAt_iff' {f : E → F} {x : E} :
ConformalAt f x ↔ ∃ c : ℝ, 0 < c ∧ ∀ u v : E, ⟪fderiv ℝ f x u, fderiv ℝ f x v⟫ = c * ⟪u, v⟫ := by
rw [conformalAt_iff_isConformalMap_fderiv, isConformalMap_iff]
