angle_map — Mathlib

English

Let s be a subspace of V. For x, y in s, the angle between x and y considered in s equals the angle between x and y in V.

Русский

Пусть s — подпространство V. Для векторов x, y из s угол между ними в пространстве s равен углу между ними в V.

LaTeX

$$$$ \angle (x : V) (y : V) = \angle x y \quad \text{для } x,y \in s. $$$$

Lean4

@[simp]
theorem _root_.LinearIsometry.angle_map {E F : Type*} [NormedAddCommGroup E] [NormedAddCommGroup F]
    [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] (f : E →ₗᵢ[ℝ] F) (u v : E) : angle (f u) (f v) = angle u v := by
  rw [angle, angle, f.inner_map_map, f.norm_map, f.norm_map]

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