comap_le_comap_iff_of_surjective — Mathlib

English

If f is surjective, then S.comap f ≤ T.comap f if and only if S ≤ T for Submonoids S,T of N.

Русский

Пусть f сюръективен. Тогда S.comap f ≤ T.comap f эквивалентно S ≤ T для подмножество S,T в N.

LaTeX

$$$ \\forall S,T,\\; S\\!\\uparrow\\!f \\le T\\!\\uparrow\\!f \\iff S \\le T. $$$

Lean4

@[to_additive]
theorem comap_le_comap_iff_of_surjective {S T : Submonoid N} : S.comap f ≤ T.comap f ↔ S ≤ T :=
  (giMapComap hf).u_le_u_iff

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