angle_coe — Mathlib

English

If x and y are elements of a subspace (viewed as vectors), then the angle between their ambient representatives equals the angle between x and y inside the subspace.

Русский

Если x и y — элементы подпространства (как векторы), то угол между их образами во внешнем пространстве совпадает с углом между x и y внутри подпространства.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem _root_.Submodule.angle_coe {s : Submodule ℝ V} (x y : s) : angle (x : V) (y : V) = angle x y :=
  s.subtypeₗᵢ.angle_map x y

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