map_le_iff_le_comap — Mathlib

English

Let f be a multiplicative homomorphism between semigroup structures on M and N. For any subsemigroups S of M and T of N, S maps into T if and only if S is contained in the preimage of T under f.

Русский

Пусть f — мультипликативный гомоморфизм между полугруппами M и N. Для любых подполугрупп S ⊆ M и T ⊆ N выполняется: образ S через f лежит внутри T тогда и только тогда, когда S ⊆ f^{-1}(T).

LaTeX

$$$S.map\ f \le T \Longleftrightarrow S \le T .comap\ f$$$

Lean4

@[to_additive]
theorem map_le_iff_le_comap {f : M →ₙ* N} {S : Subsemigroup M} {T : Subsemigroup N} : S.map f ≤ T ↔ S ≤ T.comap f :=
  image_subset_iff

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