map_le_map_iff_of_injective — Mathlib

English

Let f: M → N be an injective semigroup homomorphism. For all subsemigroups S, T of M, the image under f satisfies S.map f ≤ T.map f if and only if S ≤ T. In other words, the map S ↦ S.map f is order-embedding on subsemigroups when f is injective.

Русский

Пусть f: M → N — инъективное полугрупповое отображение. Для любых подполугрупп S, T ⊆ M верно: S.map f ≤ T.map f тогда и только если S ≤ T. Другими словами, отображение S ↦ S.map f остаётся вложением порядка на подполугруппах при инъективности f.

LaTeX

$$$\\operatorname{Injective}(f) \\rightarrow \\forall \\{S,T\\} \\ Subsemigroup(M),\\ S.map\,f \\le T.map\,f \\iff S \\le T$$$

Lean4

@[to_additive]
theorem map_le_map_iff_of_injective {S T : Subsemigroup M} : S.map f ≤ T.map f ↔ S ≤ T :=
  (gciMapComap hf).l_le_l_iff

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