subtypeₐᵢ_linearIsometry — Mathlib

English

For any affine subspace s, the linearIsometry part of the subtype map s.subtype_AI equals the linearIsometry part of the direction’s subtype.

Русский

Для любого аффинного подпространства s линейная изометрия отображения-подтипа s.subtype_AI совпадает с линейной изометрией подтипа направления s.

LaTeX

$$$$ (s.\mathrm{subtype}_{AI})^{\mathrm{linearIsometry}} = (s.\mathrm{direction}.\mathrm{subtype}_{\mathrm{LI}}) $$$$

Lean4

@[simp]
theorem subtypeₐᵢ_linearIsometry (s : AffineSubspace 𝕜 P) [Nonempty s] :
    s.subtypeₐᵢ.linearIsometry = s.direction.subtypeₗᵢ :=
  rfl

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