map_le_of_le_comap — Mathlib

English

If S is a subsemigroup of M and T is a subsemigroup of N, then whenever S is contained in the comap of T along f, the image S.map f is contained in T; conversely, containment of S.map f in T implies containment of S in comap f T.

Русский

Пусть S ⊆ M и T ⊆ N. Если S ⊆ T comap f, то S.map f ⊆ T, и наоборот: если S.map f ⊆ T, то S ⊆ T.comap f.

LaTeX

$$$S \le T.{\mathrm{comap}}\ f \;\Rightarrow\; S.map\ f \le T \\ S.map\ f \le T \Rightarrow S \le T.{\mathrm{comap}}\ f$$

Lean4

@[to_additive]
theorem map_le_of_le_comap {T : Subsemigroup N} {f : M →ₙ* N} : S ≤ T.comap f → S.map f ≤ T :=
  (gc_map_comap f).l_le

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