InnerProductGeometry.ConformalAt.preserves_angle

theorem InnerProductGeometry.ConformalAt.preserves_angle : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] {f : E → F} {x : E} {f' : E →L[ℝ] F}, HasFDerivAt f f' x → ConformalAt f x → ∀ (u v : E), InnerProductGeometry.angle (f' u) (f' v) = InnerProductGeometry.angle u v

This theorem states that if a real differentiable map `f` is conformal at a point `x`, it preserves the angles at that point. More specifically, for all vectors `u` and `v` originating from `x`, the angle between the images of `u` and `v` under the derivative map `f'` is the same as the original angle between `u` and `v`. The map is confirmed to be conformal at `x` by the predicate `ConformalAt f x`, and the derivative of `f` at `x` is given by `f'` (`HasFDerivAt f f' x`). Here, the angle is measured using the `InnerProductGeometry.angle` function, which computes the undirected angle between two vectors.

More concisely: If a real differentiable function `f` is conformal at a point `x`, then the angle between the derivatives of any two vectors at `x` is equal to the angle between the vectors themselves.