map_inl — Mathlib

English

If f is a monoid equivalence f: M ≃* N, then K.map f = K.comap f.symm for any submonoid K ⊆ M.

Русский

Если f — эквивалент моноидов f: M ≃* N, то для любого подмоноида K ⊆ M выполняется K.map f = K.comap f.symm.

LaTeX

$$$ K.map f = K.comap f.symm. $$$

Lean4

@[to_additive]
theorem map_inl (s : Submonoid M) : s.map (inl M N) = s.prod ⊥ :=
  ext fun p =>
    ⟨fun ⟨_, hx, hp⟩ => hp ▸ ⟨hx, Set.mem_singleton 1⟩, fun ⟨hps, hp1⟩ =>
      ⟨p.1, hps, Prod.ext rfl <| (Set.eq_of_mem_singleton hp1).symm⟩⟩

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