subsemigroupMap — Mathlib

Lean4
/-- A `MulEquiv` `φ` between two semigroups `M` and `N` induces a `MulEquiv` between
a subsemigroup `S ≤ M` and the subsemigroup `φ(S) ≤ N`.
See `MulHom.subsemigroupMap` for a variant for `MulHom`s. -/
@[to_additive (attr := simps) /-- An `AddEquiv` `φ` between two additive semigroups `M` and `N` induces an `AddEquiv`
          between a subsemigroup `S ≤ M` and the subsemigroup `φ(S) ≤ N`.
          See `AddHom.addSubsemigroupMap` for a variant for `AddHom`s. -/
    ]
def subsemigroupMap (e : M ≃* N) (S : Subsemigroup M) : S ≃* S.map (e : M →ₙ* N) :=
  { -- we restate this for `simps` to avoid `⇑e.symm.toEquiv x`
    (e : M →ₙ* N).subsemigroupMap S,
    (e : M ≃ N).image S with
    toFun := fun x => ⟨e x, _⟩
    invFun := fun x => ⟨e.symm x, _⟩ }
Похожие утверждения