const_apply — Mathlib

English

The constant function to a fixed point p ∈ P2 yields an affine map P1 →ᵃ[k] P2 whose toFun is the constant function with value p, and whose linear part is zero.

Русский

Постоянное отображение в фиксированную точку p ∈ P2 задаёт аффинное отображение P1 →ᵃ[k] P2, у которого toFun равно константе p и линейная часть равна нулю.

LaTeX

$$def const (p : P2) : P1 →ᵃ[k] P2 where toFun := Function.const P1 p; linear := 0; map_vadd' _ _ := by simp$$

Lean4

@[simp]
theorem const_apply (p : P2) (q : P1) : (const k P1 p) q = p :=
  rfl

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