fromEdgeSet_sdiff — Mathlib

English

FromEdgeSet distributes over set difference: fromEdgeSet(s \\ t) equals fromEdgeSet(s) \\ fromEdgeSet(t).

Русский

FromEdgeSet распределяется по разности множеств: fromEdgeSet(s \\ t) = fromEdgeSet(s) \\ fromEdgeSet(t).

LaTeX

$$$\\mathrm{fromEdgeSet}(s \\\\ t) = \\mathrm{fromEdgeSet}(s) \\\\ \\mathrm{fromEdgeSet}(t)$$$

Lean4

@[simp]
theorem fromEdgeSet_sdiff (s t : Set (Sym2 V)) : fromEdgeSet (s \ t) = fromEdgeSet s \ fromEdgeSet t :=
  by
  ext v w
  constructor <;> simp +contextual

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