map_comap_eq_self

Mathlib.Algebra.Group.Subsemigroup.Operations

URI: https://scilib.ai/kg/mathlib#Subsemigroup.map_comap_eq_self

← MathLib Explorer

English

If S is contained in the srange of f, then map(comap f S) = S.

Русский

Если S ⊆ f.srange, то map (comap f S) = S.

LaTeX

$$$S \le f.srange \Rightarrow (S.comap f).map f = S$$$

Lean4

@[to_additive]
theorem map_comap_eq_self {f : M →ₙ* N} {S : Subsemigroup N} (h : S ≤ f.srange) : (S.comap f).map f = S := by
  simpa only [inf_of_le_left h] using map_comap_eq f S

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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