coeAddHom — Mathlib

English

There is an additive homomorphism from sections to dependent maps given by evaluation: coeAddHom(s) is the map x ↦ s(x).

Русский

Существует аддитивное гомоморфное отображение от секций к зависимым отображениям, заданное по значению: coeAddHom(s) — это отображение x ↦ s(x).

LaTeX

$$$$ \operatorname{coeAddHom}(s) = s $$$$

Lean4

/-- The additive morphism from `C^n` sections to dependent maps. -/
def coeAddHom : Cₛ^n⟮I; F, V⟯ →+ ∀ x, V x where
  toFun := (↑)
  map_zero' := coe_zero
  map_add' := coe_add

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