induceHom_id — Mathlib

English

The restriction of the identity graph morphism to induced subgraphs is the identity morphism.

Русский

Ограничение тождественного гомоморфизма графов на индуцированные подграфы даёт тождественный гомоморфизм.

LaTeX

$$$ \mathrm{induceHom}\big( \mathrm{Hom.id}: G \to_g G \big) \big( s \big) = \mathrm{Hom.id} $$$

Lean4

@[simp]
theorem induceHom_id (G : SimpleGraph V) (s) : induceHom (Hom.id : G →g G) (Set.mapsTo_id s) = Hom.id :=
  by
  ext x
  rfl

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