edgeSet_fromEdgeSet — Mathlib

English

The edge set of fromEdgeSet(s) equals s with all diagonals removed.

Русский

Множество рёбер графа fromEdgeSet(s) равно множеству rёбер s за вычетом диагоналей.

LaTeX

$$$\\mathrm{edgeSet}(\\mathrm{fromEdgeSet}(s)) = s \\setminus \\{ e : \\mathrm{Sym}^2 V \\mid e.\\mathrm{IsDiag} \\}$$$

Lean4

@[simp]
theorem edgeSet_fromEdgeSet : (fromEdgeSet s).edgeSet = s \ {e | e.IsDiag} :=
  by
  ext e
  exact Sym2.ind (by simp) e

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