map_constants

Mathlib.ModelTheory.Basic

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Equiv.map_constants

English

Let φ: M ≃[L] N. Then φ maps each interpretation of a constant c to itself: φ(c^M) = c^N.

Русский

Пусть φ: M ≃_L N. Тогда φ переводит каждую интерпретацию константы c в саму константу: φ(c^M) = c^N.

LaTeX

$$$\phi\bigl(c^M\bigr) = c^N$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru