case Adj.h.h.a
ι : Sort ?u.82740
𝕜 : Type ?u.82743
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 : Set (Sym2 V)
v w : V
⊢ Adj (fromEdgeSet ∅) v w ↔ Adj ⊥ v w
ι : Sort ?u.82740
𝕜 : Type ?u.82743
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 : Set (Sym2 V)
⊢ fromEdgeSet ∅ = ⊥
ext (v w)
no goals
case Adj.h.h.a
ι : Sort ?u.82740
𝕜 : Type ?u.82743
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 : Set (Sym2 V)
v w : V
⊢ Adj (fromEdgeSet ∅) v w ↔ Adj ⊥ v w
simp only [fromEdgeSet_adj, Set.mem_empty_iff_false, false_and_iff, bot_adj]