subtypeₐᵢ_linear — Mathlib

English

For any affine subspace s of P, the linear part of the subtype map s.subtype_AI equals the subtype of the direction of s.

Русский

Пусть s — аффинное подпространство пространства P. Линейная часть отображения-подтипа s.subtype_AI равна подтипу направления s.

LaTeX

$$$$ s.\mathrm{subtype}_{AI}^{\mathrm{linear}} = s.\mathrm{direction}.\mathrm{subtype}. $$$$

Lean4

theorem subtypeₐᵢ_linear (s : AffineSubspace 𝕜 P) [Nonempty s] : s.subtypeₐᵢ.linear = s.direction.subtype :=
  rfl

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