map_equiv_top — Mathlib

English

Let f be a multiplicative equivalence between M and N. Then the image of the top submonoid of M under f is the top submonoid of N: (⊤ : Submonoid M).map f = ⊤.

Русский

Пусть f — моноидная эквиваленция между M и N. Образ верхнего подмонойдa M равен верхнему подмонойду N: (⊤ : Submonoid M).map f = ⊤.

LaTeX

$$$$ (\\top : \\mathrm{Submonoid}(M)).\\mathrm{map}\,f = \\top $$$$

Lean4

@[to_additive (attr := simp)]
theorem map_equiv_top (f : M ≃* N) : (⊤ : Submonoid M).map f = ⊤ :=
  SetLike.coe_injective <| Set.image_univ.trans f.surjective.range_eq

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