map_iSup

Mathlib.ModelTheory.Substructures

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

English

Mapping commutes with arbitrary infima of substructures.

Русский

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

LaTeX

$$$\\mathrm{map}\,f\\,\\bigwedge_i s_i = \\bigwedge_i (\\mathrm{map}\,f\\,s_i)$$$

Lean4

theorem map_iSup {ι : Sort*} (f : M →[L] N) (s : ι → L.Substructure M) : (⨆ i, s i).map f = ⨆ i, (s i).map f :=
  (gc_map_comap f).l_iSup

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

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

Разделы

Аффилиация

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