Theorems · Theorem · geometry

Orientation.oangle_map

∀ {V : Type u_1} {V' : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedAddCommGroup V']
  [inst_2 : InnerProductSpace ℝ V] [inst_3 : InnerProductSpace ℝ V'] [inst_4 : Fact (Module.finrank ℝ V = 2)]
  [inst_5 : Fact (Module.finrank ℝ V' = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V') (f : V ≃ₗᵢ[ℝ] V'),
  ((Orientation.map (Fin 2) f.toLinearEquiv) o).oangle x y = o.oangle (f.symm x) (f.symm y)

The angle between two vectors, with respect to an orientation given by Orientation.map with a linear isometric equivalence, equals the angle between those two vectors, transformed by the inverse of that equivalence, with respect to the original orientation.

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Cited by

1 results in Mathlib

Foundations

Depth 254 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedAddCommGroupInnerProductSpaceInnerProductSpaceFactFact