le_comap_map — Mathlib

English

For a subsemigroup S of M, the map operation followed by comap does not exceed identity: (S.map f).comap f ≤ S; equivalently, the composite map followed by comap is monotone.

Русский

Для подполугруппы S ⊆ M выполняется (S.map f).comap f ≤ S, то есть композиция образа и обратного образа относительно f не превосходит тождественного отображения.

LaTeX

$$((S.map f).comap f) ≤ S$$

Lean4

@[to_additive]
theorem le_comap_map {f : M →ₙ* N} : S ≤ (S.map f).comap f :=
  (gc_map_comap f).le_u_l _

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