edgeSet_subset_edgeSet

Mathlib.Combinatorics.SimpleGraph.Basic

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

English

E(G1) ⊆ E(G2) iff G1 ≤ G2.

Русский

Mножество ребер G1 подмножество множества ребер G2 тогда и только тогда, когда G1 ≤ G2.

LaTeX

$$$$ E(G_1) \subseteq E(G_2) \iff G_1 \le G_2. $$$$

Lean4

@[simp]
theorem edgeSet_subset_edgeSet : edgeSet G₁ ⊆ edgeSet G₂ ↔ G₁ ≤ G₂ :=
  (edgeSetEmbedding V).le_iff_le

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

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

Разделы

Аффилиация

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