induceHom — Mathlib

English

The restriction of a graph morphism φ: G →g G' to induced subgraphs G.induce s →g G'.induce t is defined when φ maps s into t.

Русский

Ограничение гомоморфизма φ на индуцированные подграфы G.induce s →g G'.induce t определено при том, что φ отображает s в t.

LaTeX

$$$ \mathrm{induceHom} : G.induce s \to_g G'.induce t $$$

Lean4

/-- The restriction of a morphism of graphs to induced subgraphs. -/
def induceHom : G.induce s →g G'.induce t
    where
  toFun := Set.MapsTo.restrict φ s t φst
  map_rel' := φ.map_rel'

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