constants_mem

Mathlib.ModelTheory.Substructures

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Substructure.constants_mem

English

Every constant of L maps to an element of S.

Русский

Каждая константа языка L отображается в элемент S.

LaTeX

$$$$ c \in S $$$$

Lean4

theorem constants_mem (c : L.Constants) : (c : M) ∈ S :=
  mem_carrier.2 (S.fun_mem c _ finZeroElim)

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

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

Разделы

Аффилиация

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