le_comap_of_map_le — Mathlib

English

The leq (less-or-equal) relation respects comap and map in both directions: if S.map f ≤ T, then S ≤ T.comap f, and dually, if S ≤ T.comap f then S.map f ≤ T.

Русский

Отношение ⊆ сохраняет направленность через comap и map: если S.map f ≤ T, то S ≤ T.comap f, и наоборот.

LaTeX

$$$S.map f \le T \Rightarrow S \le T.comap f \quad\text{and}\quad S \le T.comap f \Rightarrow S.map f \le T$$

Lean4

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

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