le_comap_map

Mathlib.Algebra.Group.Submonoid.Operations

URI: https://scilib.ai/kg/mathlib#Submonoid.le_comap_map

English

For any submonoid S of M, we have S ≤ (S.map f).comap f; i.e., S is contained in the preimage of its image.

Русский

Для любого подмоноида S ⊆ M имеем S ⊆ (S.map f).comap f; то есть S содержится в предобразе образа S.

LaTeX

$$$S \le (S.\mathrm{map}\!\_f).\mathrm{comap}\!\_f$$$

Lean4

@[to_additive]
theorem le_comap_map {f : F} : S ≤ (S.map f).comap f :=
  (gc_map_comap f).le_u_l _

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

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

Разделы

Аффилиация

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