hom — Mathlib

English

There exists an induced injective graph homomorphism from any subgraph x into G, given by the vertex-restricting inclusion.

Русский

С любого подграфа x графа G существует индуцированный инъективный граф-гомоморфизм x → G, задаваемый включением вершин.

LaTeX

$$$\forall x : \text{Subgraph}(G),\ \exists \phi: x.\,\mathrm{coe} \to G,\ \phi\text{ граф-гомоморфизм и инъективен}.$$$

Lean4

/-- There is an induced injective homomorphism of a subgraph of `G` into `G`. -/
@[simps]
protected def hom (x : Subgraph G) : x.coe →g G where
  toFun v := v
  map_rel' := x.adj_sub

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