comap_iInf

Mathlib.ModelTheory.Substructures

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

English

Comap commutes with arbitrary sups, i.e., supremum of comaps.

Русский

Обратное отображение совместимо с верхними гранями, т. е. с supremum.

LaTeX

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

Lean4

theorem comap_iInf {ι : Sort*} (f : M →[L] N) (s : ι → L.Substructure N) : (⨅ i, s i).comap f = ⨅ i, (s i).comap f :=
  (gc_map_comap f).u_iInf

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

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

Разделы

Аффилиация

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