case Adj.h.h.a
ι : Sort ?u.85886
𝕜 : Type ?u.85889
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
s✝ s t : Set (Sym2 V)
v w : V
⊢ Adj (fromEdgeSet s ⊔ fromEdgeSet t) v w ↔ Adj (fromEdgeSet (s ∪ t)) v w
ι : Sort ?u.85886
𝕜 : Type ?u.85889
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
s✝ s t : Set (Sym2 V)
⊢ fromEdgeSet s ⊔ fromEdgeSet t = fromEdgeSet (s ∪ t)
ext (v w)
no goals
case Adj.h.h.a
ι : Sort ?u.85886
𝕜 : Type ?u.85889
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
s✝ s t : Set (Sym2 V)
v w : V
⊢ Adj (fromEdgeSet s ⊔ fromEdgeSet t) v w ↔ Adj (fromEdgeSet (s ∪ t)) v w
simp [Set.mem_union, or_and_right]