case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
⊢ ↑(↑(orthogonalProjection s) ↑(↑(orthogonalProjection s) p)) = ↑(↑(orthogonalProjection s) p)
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
⊢ ↑(orthogonalProjection s) ↑(↑(orthogonalProjection s) p) = ↑(orthogonalProjection s) p
ext
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
⊢ ↑(↑(orthogonalProjection s) p) ∈ s
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
⊢ ↑(↑(orthogonalProjection s) ↑(↑(orthogonalProjection s) p)) = ↑(↑(orthogonalProjection s) p)
rw [orthogonalProjection_eq_self_iff]
no goals
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
⊢ ↑(↑(orthogonalProjection s) p) ∈ s
exact orthogonalProjection_mem p