V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₁ }
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
⊢ ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) ∈ s₂
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₁ }
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
⊢ ↑(reflection s₁) p ∈ s₂
rw [reflection_apply]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₁ }
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
ho : ↑(↑(orthogonalProjection s₁) p) ∈ s₂
⊢ ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) ∈ s₂
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₁ }
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
⊢ ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) ∈ s₂
have ho : ↑(orthogonalProjection s₁ p) ∈ s₂ := hle (orthogonalProjection_mem p)
no goals
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₁ }
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
ho : ↑(↑(orthogonalProjection s₁) p) ∈ s₂
⊢ ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) ∈ s₂
exact vadd_mem_of_mem_direction (vsub_mem_direction ho hp) ho