funMap_eq_coe_constants — Mathlib

English

Let L be a language with constants and M an L-structure. For any constant symbol c ∈ L.Constants and any x in Fin(0) → M, the interpretation of c is independent of x, hence funMap c x = c.

Русский

Пусть L — язык, имеющий константы, и M — структура над L. Для любой константы c ∈ L.Constants и любого x ∈ Fin(0) → M выполняется, что интерпретация константы равна самой константе: funMap c x = c.

LaTeX

$$$\\mathrm{funMap}\\, c\\, x = c$$$

Lean4

theorem funMap_eq_coe_constants {c : L.Constants} {x : Fin 0 → M} : funMap c x = c :=
  congr rfl (funext finZeroElim)

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