edgeSet_fromEdgeSet_incidenceSet — Mathlib

English

The edge set of the graph formed from the incidence set of x coincides with the incidence set itself.

Русский

Множество ребер графа, полученного из инцидентного множества x, совпадает с самим инцидентным множеством.

LaTeX

$$$ \mathrm{edgeSet}(\mathrm{fromEdgeSet}(\mathrm{incidenceSet}(x))) = \mathrm{incidenceSet}(x) $$$

Lean4

theorem edgeSet_fromEdgeSet_incidenceSet (G : SimpleGraph V) (x : V) :
    (fromEdgeSet (G.incidenceSet x)).edgeSet = G.incidenceSet x :=
  by
  rw [edgeSet_fromEdgeSet, sdiff_eq_left, ← Set.subset_compl_iff_disjoint_right, Set.compl_setOf]
  exact (incidenceSet_subset G x).trans G.edgeSet_subset_setOf_not_isDiag

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