leftStructure

Mathlib.ModelTheory.Bundled

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Theory.ModelType.leftStructure

Lean4

instance leftStructure {L' : Language} {T : (L.sum L').Theory} (M : T.ModelType) : L.Structure M :=
  (LHom.sumInl : L →ᴸ L.sum L').reduct M

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

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

Разделы

Аффилиация

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