map_inf_comap_of_surjective — Mathlib

English

For S,T subsemigroups of N, (S.comap f ∩ T.comap f).map f = S ∩ T when f is surjective.

Русский

Для подполугрупп S,T в N, при сюръективности f выполняется (S.comap f ∩ T.comap f).map f = S ∩ T.

LaTeX

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

Lean4

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

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