coe_apply — Mathlib

English

The restriction of an affine map to a subspace E is compatible with evaluation: the underlying value equals the value of φ on x.

Русский

Ограничение аффинного отображения к подпространству E совместимо с применением к точке x.

LaTeX

$$$ ↑(\\phi.restrict hEF x) = \\phi x $$$

Lean4

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

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