fromEdgeSet_union — Mathlib

English

FromEdgeSet distributes over union: fromEdgeSet(s ∪ t) equals fromEdgeSet(s) ⊔ fromEdgeSet(t).

Русский

FromEdgeSet распределяется по объединению: fromEdgeSet(s ∪ t) = fromEdgeSet(s) ⊔ fromEdgeSet(t).

LaTeX

$$$\\mathrm{fromEdgeSet}(s \\cup t) = \\mathrm{fromEdgeSet}(s) \\; \\sup \\; \\mathrm{fromEdgeSet}(t)$$$

Lean4

@[simp]
theorem fromEdgeSet_union (s t : Set (Sym2 V)) : fromEdgeSet (s ∪ t) = fromEdgeSet s ⊔ fromEdgeSet t :=
  by
  ext v w
  simp [Set.mem_union, or_and_right]

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