mapSpanningSubgraphs_inj — Mathlib

English

If G ≤ G', the inclusion map of subgraphs is injective.

Русский

Если G является подграфом G', то естественный включающий морфизм подграфов инъективен.

LaTeX

$$$ \\text{Injective}(\\mathrm{ofLE}\\; h) $$$

Lean4

@[deprecated "This is true by simp" (since := "2025-03-17")]
theorem mapSpanningSubgraphs_inj {G G' : SimpleGraph V} {v w : V} (h : G ≤ G') : ofLE h v = ofLE h w ↔ v = w := by simp

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