fromEdgeSet_inter — Mathlib

English

FromEdgeSet distributes over intersection: fromEdgeSet(s ∩ t) equals fromEdgeSet(s) ⊓ fromEdgeSet(t).

Русский

FromEdgeSet распределяется по пересечению: fromEdgeSet(s ∩ t) = fromEdgeSet(s) ⊓ fromEdgeSet(t).

LaTeX

$$$\\mathrm{fromEdgeSet}(s \\cap t) = \\mathrm{fromEdgeSet}(s) \\; \\inf \\; \\mathrm{fromEdgeSet}(t)$$$

Lean4

@[simp]
theorem fromEdgeSet_inter (s t : Set (Sym2 V)) : fromEdgeSet (s ∩ t) = fromEdgeSet s ⊓ fromEdgeSet t :=
  by
  ext v w
  simp only [fromEdgeSet_adj, Set.mem_inter_iff, Ne, inf_adj]
  tauto

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