coe_isContained

Mathlib.Combinatorics.SimpleGraph.Copy

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Subgraph.coe_isContained

English

For any subgraph G' of G, the coerced copy G'.coe is contained in G.

Русский

Для любого подграфа G' графа G его приводимая копия G'.coe содержится в G.

LaTeX

$$G'.coe ⊑ G$$

Lean4

/-- A simple graph `G` contains all `Subgraph G` coercions. -/
theorem coe_isContained (G' : G.Subgraph) : G'.coe ⊑ G :=
  ⟨G'.coeCopy⟩

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

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

Разделы

Аффилиация

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