map_inf_comap_of_surjective — Mathlib

English

Let f be a surjective monoid hom. For any S,T ⊆ N, the image under map f of the infimum (intersection) of comaps equals the infimum of the original submonoids: map f (comap f S ∩ comap f T) = S ∩ T.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem map_inf_comap_of_surjective (S T : Submonoid N) : (S.comap f ⊓ T.comap f).map f = S ⊓ T :=
  (giMapComap hf).l_inf_u _ _

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