comap_sup_map_of_injective — Mathlib

English

If f is injective, comap distributes over supremum of images: comap f (map f S ⊔ map f T) = S ⊔ T.

Русский

При инъекции f, предобраз через f распределяется по супремуму образов: comap f (map f S ⊔ map f T) = S ⊔ T.

LaTeX

$$$\mathrm{comap}\!\_f (\mathrm{map}\!\_f S \sqcup \mathrm{map}\!\_f T) = S \sqcup T$ (при инъективности f)$$

Lean4

@[to_additive]
theorem comap_sup_map_of_injective (S T : Submonoid M) : (S.map f ⊔ T.map f).comap f = S ⊔ T :=
  (gciMapComap hf).u_sup_l _ _

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