disjoint_fromEdgeSet — Mathlib

English

Disjoint G and fromEdgeSet s holds iff s and G.edgeSet are disjoint.

Русский

Пусть G — граф; тогда Disjoint(G, fromEdgeSet(s)) эквивалентно Disjoint(s, G.edgeSet).

LaTeX

$$$\\operatorname{Disjoint}(G, \\mathrm{fromEdgeSet}(s)) \\iff \\operatorname{Disjoint}(s, G.\\mathrm{edgeSet})$$$

Lean4

@[simp]
theorem disjoint_fromEdgeSet : Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet s :=
  by
  conv_rhs => rw [← Set.diff_union_inter s {e : Sym2 V | e.IsDiag}]
  rw [← disjoint_edgeSet, edgeSet_fromEdgeSet, Set.disjoint_union_right, and_iff_left]
  exact Set.disjoint_left.2 fun e he he' ↦ not_isDiag_of_mem_edgeSet _ he he'.2

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