map_bot

Mathlib.ModelTheory.Substructures

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

English

Mapping the bottom substructure yields the bottom substructure.

Русский

Образ нижней подструктуры при отображении отображается в нижнюю подструктуру.

LaTeX

$$$(\\bot : L.Substructure M).map f = \\bot$$$

Lean4

@[simp]
theorem map_bot (f : M →[L] N) : (⊥ : L.Substructure M).map f = ⊥ :=
  (gc_map_comap f).l_bot

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

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

Разделы

Аффилиация

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