support_mono

Mathlib.Combinatorics.SimpleGraph.Basic

URI: https://scilib.ai/kg/mathlib#SimpleGraph.support_mono

English

If G is contained in G' (G ≤ G'), then every edge of G is also an edge of G'.

Русский

Если граф G вложен в граф G' (G ≤ G'), то множество ребер G содержится в множестве ребер G'.

LaTeX

$$$$ G \le G' \Rightarrow E(G) \subseteq E(G'). $$$$

Lean4

theorem support_mono {G G' : SimpleGraph V} (h : G ≤ G') : G.support ⊆ G'.support :=
  SetRel.dom_mono fun _uv huv ↦ h huv

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru