linear — Mathlib

English

The linear part of the restricted affine map is the restriction of φ.linear to the appropriate comap space.

Русский

Линейная часть ограниченного аффинного отображения является ограничением φ.linear на соответствующее пространство.

LaTeX

$$$ (\\phi.restrict hEF).linear = \\phi.linear.restrict (AffineMap.restrict.linear_aux hEF) $$$

Lean4

theorem linear (φ : P₁ →ᵃ[k] P₂) {E : AffineSubspace k P₁} {F : AffineSubspace k P₂} [Nonempty E] [Nonempty F]
    (hEF : E.map φ ≤ F) : (φ.restrict hEF).linear = φ.linear.restrict (AffineMap.restrict.linear_aux hEF) :=
  rfl

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