English
Let E and F be real inner product spaces and f : E → F differentiable at x with derivative f' : E →L[ℝ] F. If H is a conformal at x for f, then for all u, v ∈ E one has ⟪f' u, f' v⟫ = (conformalFactorAt H) · ⟪u, v⟫.
Русский
Пусть E и F — вещественные пространства с внутренним произведением, f : E → F дифференцируема в точке x с производной f'. Если f конформна в x с соответствующим фактором конформности H, то для всех u, v ∈ E выполнено ⟪f' u, f' v⟫ = (conformalFactorAt(H)) · ⟪u, v⟫.
LaTeX
$$$\\langle f' u, f' v \\rangle = (\\operatorname{conformalFactorAt}(H)) \\cdot \\langle u, v \\rangle$$$
Lean4
theorem conformalFactorAt_inner_eq_mul_inner {f : E → F} {x : E} {f' : E →L[ℝ] F} (h : HasFDerivAt f f' x)
(H : ConformalAt f x) (u v : E) : ⟪f' u, f' v⟫ = (conformalFactorAt H : ℝ) * ⟪u, v⟫ :=
H.differentiableAt.hasFDerivAt.unique h ▸ conformalFactorAt_inner_eq_mul_inner' H u v
