prod_top — Mathlib

English

The top of the product of a top submonoid on M with a submonoid on N is the comap of fst.

Русский

Верхняя часть произведения верхнего подмоноида на M и подмножества на N равна обратному образу fst.

LaTeX

$$$ (\top : Submonoid M).prod S = S\,\text{comap}\,\mathrm{fst}. $$$

Lean4

@[to_additive prod_top]
theorem prod_top (s : Submonoid M) : s.prod (⊤ : Submonoid N) = s.comap (MonoidHom.fst M N) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_fst]

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