map_constants — Mathlib

English

If φ is an L-elementary embedding from M to N, then φ fixes every constant symbol of the language, i.e., φ(c)=c for all constants c in L.

Русский

Пусть φ — элементарное вложение M в N для языка L; тогда φ фиксирует все константы языка: φ(c)=c для каждого константного символа c.

LaTeX

$$$$ \\forall c \\in L.const, \\; \\varphi(c)=c.$$$

Lean4

@[simp]
theorem map_constants (φ : M ↪ₑ[L] N) (c : L.Constants) : φ c = c :=
  HomClass.map_constants φ c

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