map_comap_le

Mathlib.ModelTheory.Substructures

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

English

For S: L.Substructure M, f: M →[L] N, map f then comap f is bounded

Русский

Для S: подструктура M и отображения f, ограничение map f и comap f дает границы

LaTeX

$$$(S.map f).comap f \\le S$$$

Lean4

theorem map_comap_le {S : L.Substructure N} {f : M →[L] N} : (S.comap f).map f ≤ S :=
  (gc_map_comap f).l_u_le _

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

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

Разделы

Аффилиация

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