rightStructure

Mathlib.ModelTheory.Bundled

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

Lean4

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

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

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

Разделы

Аффилиация

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