Theorems · Theorem · geometry

Affine.Simplex.orthogonalProjectionSpan_eq_point

∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : Affine.Simplex 𝕜 P 0)
  (p : P), ↑(s.orthogonalProjectionSpan p) = s.points 0

Defined in: Mathlib.Geometry.Euclidean.Projection
Cited by: 2 results in Mathlib
Foundations: Depth 183 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: RCLike NormedAddCommGroup InnerProductSpace MetricSpace NormedAddTorsor

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites23

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setproof · cited by 53,352
Moduleproof · cited by 20,661
NormedAddCommGroupstatement and proof · cited by 15,752
AddCommGroupproof · cited by 12,871
Ringproof · cited by 7,463
Submodulestatement · cited by 7,192
Set.rangestatement and proof · cited by 4,705
InnerProductSpacestatement and proof · cited by 3,523
RCLikestatement and proof · cited by 2,829
MetricSpacestatement and proof · cited by 1,684
AddTorsorproof · cited by 1,657

Cited by2

Results whose statement or proof uses this declaration.

Affine.Simplex.orthogonalProjectionSpan_faceOpposite_eq_point_revproof · cited by 1
Affine.Simplex.altitudeFoot_eq_point_revproof · cited by 1