Theorems · Theorem · geometry

EuclideanGeometry.two_zsmul_oangle_self_orthogonalProjection

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)] (p : P)
  {p' : P} {s : AffineSubspace ℝ P} [inst_5 : s.direction.HasOrthogonalProjection],
  p ∉ s →
    ∀ (h : p' ∈ s),
      p' ≠ ↑((EuclideanGeometry.orthogonalProjection s) p) →
        2 • EuclideanGeometry.oangle p (↑((EuclideanGeometry.orthogonalProjection s) p)) p' = ↑Real.pi

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Projection

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorFactModule.OrientedSubmodule.HasOrthogonalProjection