top_prod — Mathlib

English

The top subsemigroup in the product is the comap of the first projection applied to the top subsemigroup in M.

Русский

Верхняя подполугруппа в произведении равна образу от проекции на первый фактор.

LaTeX

$$⊤.prod S = comap (MulHom.fst M N) S$$

Lean4

@[to_additive top_prod]
theorem top_prod (s : Subsemigroup N) : (⊤ : Subsemigroup M).prod s = s.comap (MulHom.snd M N) :=
  ext fun x => by simp [mem_prod, MulHom.coe_snd]

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