disjoint_edgeSet — Mathlib

English

Disjoint E(G1) and E(G2) iff Disjoint G1 and G2.

Русский

Рёбра графов G1 и G2 не пересекаются эквивалентно тому, что сами графы не пересекаются.

LaTeX

$$$$ \text{Disjoint}(E(G_1), E(G_2)) \iff \text{Disjoint}(G_1, G_2). $$$$

Lean4

@[simp]
theorem disjoint_edgeSet : Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂ := by
  rw [Set.disjoint_iff, disjoint_iff_inf_le, ← edgeSet_inf, ← edgeSet_bot, ← Set.le_iff_subset,
    OrderEmbedding.le_iff_le]

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