edgeFinset_subset_edgeFinset

Mathlib.Combinatorics.SimpleGraph.Finite

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

English

Subsetting edgeFinsets corresponds exactly to the partial order on graphs.

Русский

Подмножество edgeFinset соответствует отношению порядка графов.

LaTeX

$$$G_1.edgeFinset \\subseteq G_2.edgeFinset \\iff G_1 \\le G_2$$$

Lean4

theorem edgeFinset_subset_edgeFinset : G₁.edgeFinset ⊆ G₂.edgeFinset ↔ G₁ ≤ G₂ := by simp

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

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

Разделы

Аффилиация

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