conformalFactorAt_inner_eq_mul_inner'

English

A restatement: for h conformal at x, the inner products under fderiv at x satisfy the relation with conformalFactorAt h.

Русский

Переформулировка: если h конформно в x, то ⟪fderiv x u, fderiv x v⟫ = conformalFactorAt(h) · ⟪u,v⟫.

LaTeX

$$$ ⟪(fderiv \mathbb{R} f x) u, (fderiv \mathbb{R} f x) v\rangle = (conformalFactorAt h) ⟪u,v⟫ $$$

Lean4

theorem conformalFactorAt_inner_eq_mul_inner' {f : E → F} {x : E} (h : ConformalAt f x) (u v : E) :
    ⟪(fderiv ℝ f x) u, (fderiv ℝ f x) v⟫ = (conformalFactorAt h : ℝ) * ⟪u, v⟫ :=
  (Classical.choose_spec <| conformalAt_iff'.mp h).2 u v

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