comap_map_comap

Mathlib.ModelTheory.Substructures

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

English

Mapping commutes with arbitrary suprema of substructures.

Русский

Отображение совместимо с произвольными верхними границами подструктур.

LaTeX

$$$\\mathrm{map}\,f\\,\\left( \\bigvee_i s_i \\right) = \\bigvee_i (\\mathrm{map}\,f\\,s_i)$$$

Lean4

@[simp]
theorem comap_map_comap {S : L.Substructure N} {f : M →[L] N} : ((S.comap f).map f).comap f = S.comap f :=
  (gc_map_comap f).u_l_u_eq_u _

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

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

Разделы

Аффилиация

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