reflection_mem_of_le_of_mem — Mathlib

English

If s1 ≤ s2 and p ∈ s2, then the reflection of p in s1 lies in s2.

Русский

Если s1 ⊆ s2 и p ∈ s2, то refl_s1(p) ∈ s2.

LaTeX

$$$$\text{If } s_1 \le s_2 \text{ and } p \in s_2,\ \mathrm{reflection}_{s_1}(p) \in s_2.$$$$

Lean4

/-- The reflection of a point in a subspace is contained in any larger
subspace containing both the point and the subspace reflected in. -/
theorem reflection_mem_of_le_of_mem {s₁ s₂ : AffineSubspace ℝ P} [Nonempty s₁] [s₁.direction.HasOrthogonalProjection]
    (hle : s₁ ≤ s₂) {p : P} (hp : p ∈ s₂) : reflection s₁ p ∈ s₂ :=
  by
  rw [reflection_apply]
  have ho : ↑(orthogonalProjection s₁ p) ∈ s₂ := hle (orthogonalProjection_mem p)
  exact vadd_mem_of_mem_direction (vsub_mem_direction ho hp) ho

Похожие утверждения