inclusion — Mathlib

English

Let x and y be subgraphs of G with x ⊆ y. Then the natural inclusion map from x to y is an injective graph homomorphism.

Русский

Пусть x и y — подграфы графа G и x ⊆ y. Тогда естественное включение x в y является инъективным граф-гомоморфизмом.

LaTeX

$$$\forall x,y : \text{Subgraph}(G),\ x \le y \Rightarrow \exists \phi: x.\,\mathrm{coe} \to y.\,\mathrm{coe},\ \text{GraphHom}(\phi) \land \operatorname{Injective}(\phi).$$$

Lean4

/-- Given two subgraphs, one a subgraph of the other, there is an induced injective homomorphism of
the subgraphs as graphs. -/
@[simps]
def inclusion {x y : Subgraph G} (h : x ≤ y) : x.coe →g y.coe
    where
  toFun v := ⟨↑v, And.left h v.property⟩
  map_rel' hvw := h.2 hvw

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