preserves_angle — Mathlib

English

If a real differentiable map is conformal at a point x, then it preserves angles at x: for all u,v, angle (f'u) (f'v) = angle u v.

Русский

Если отображение гладко дифференцируемо и конформно в точке x, то оно сохраняет углы в этой точке: для любых векторов u,v углы равны.

LaTeX

$$HasFDerivAt f f' x ∧ ConformalAt f x ⟹ ∀ u,v, angle (f' u) (f' v) = angle u v$$

Lean4

theorem preserves_angle {f' : E →L[ℝ] F} (h : IsConformalMap f') (u v : E) : angle (f' u) (f' v) = angle u v :=
  by
  obtain ⟨c, hc, li, rfl⟩ := h
  exact (angle_smul_smul hc _ _).trans (li.angle_map _ _)

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