subtype_linear — Mathlib

English

For a nonempty affine subspace s, the induced linear structure on the subtype s (the inclusion map s → P) equals the natural linear structure on its direction subspace, i.e., the linear map s.subtype is identical to the linear map s.direction.subtype.

Русский

Для непустого аффинного подпространства s выражение линейной структуры, индуцированной подтипом s (включение s в P), совпадает с естественной линейной структурой его направления, то есть линейное отображение s.subtype совпадает с s.direction.subtype.

LaTeX

$$$ s.\\\\subtype .linear = s.\\\\direction .subtype $$$

Lean4

@[simp]
theorem subtype_linear (s : AffineSubspace k P) [Nonempty s] : s.subtype.linear = s.direction.subtype :=
  rfl

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