orthogonalProjection_congr — Mathlib

English

Isometry maps perpBisector p1 p2 into perpBisector (f p1) (f p2).

Русский

Изометрия отображает perpBisector p1 p2 в perpBisector f(p1) f(p2).

LaTeX

$$MapsTo f (perpBisector p1 p2) (perpBisector (f p1) (f p2))$$

Lean4

/-- Since both instance arguments are propositions, allow `simp` to rewrite them
alongside the `s` argument.

Note that without the coercion to `P`, the LHS and RHS would have different types. -/
@[congr]
theorem orthogonalProjection_congr {s₁ s₂ : AffineSubspace ℝ P} {p₁ p₂ : P} [Nonempty s₁]
    [s₁.direction.HasOrthogonalProjection] (h : s₁ = s₂) (hp : p₁ = p₂) :
    letI : Nonempty s₂ := h ▸ ‹_›
    letI : s₂.direction.HasOrthogonalProjection := h ▸ ‹_›
    (orthogonalProjection s₁ p₁ : P) = (orthogonalProjection s₂ p₂ : P) :=
  by
  subst h hp
  rfl

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