map_sup_comap_of_surjective — Mathlib

English

Let f be surjective. For S,T ⊆ N, the image of the join of comaps equals the join of the original submonoids: map f (comap f S ⊔ comap f T) = S ⊔ T.

Русский

Пусть f сюръективен. Тогда образ объединения обратных образов равен объединению исходных подмножест: map f (comap f S ⊔ comap f T) = S ⊔ T.

LaTeX

$$$ \operatorname{map} f\big(\operatorname{comap} f S \sqcup \operatorname{comap} f T\big) = S \sqcup T. $$$

Lean4

@[to_additive]
theorem map_sup_comap_of_surjective (S T : Submonoid N) : (S.comap f ⊔ T.comap f).map f = S ⊔ T :=
  (giMapComap hf).l_sup_u _ _

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