induceHomOfLE_toHom — Mathlib

English

The underlying Hom of the induced embedding equals the induced homomorphism defined by the identity on G and the mono_right inclusion of s into s'.

Русский

Базовая гомоморфия индуцированного вложения задаётся тождественным отображением на G и включением на s ⊆ s'.

LaTeX

$$$ (G.induceHomOfLE h).toHom = induceHom (\mathrm{id} : G \to_g G) ((\mathrm Set.mapsTo_id s).mono_right h)$$$

Lean4

@[simp]
theorem induceHomOfLE_toHom : (G.induceHomOfLE h).toHom = induceHom (.id : G →g G) ((Set.mapsTo_id s).mono_right h) :=
  by ext; simp

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