case h
ι : Sort ?u.140009
𝕜 : Type ?u.140012
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
G : SimpleGraph V
v w : V
⊢ w ∈ neighborSet G v ∪ neighborSet (Gᶜ) v ↔ w ∈ {v}ᶜ
ι : Sort ?u.140009
𝕜 : Type ?u.140012
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
G : SimpleGraph V
v : V
⊢ neighborSet G v ∪ neighborSet (Gᶜ) v = {v}ᶜ
ext w
case h
ι : Sort ?u.140009
𝕜 : Type ?u.140012
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
G : SimpleGraph V
v w : V
h : ∀ {a b : V}, Adj G a b → a ≠ b
⊢ w ∈ neighborSet G v ∪ neighborSet (Gᶜ) v ↔ w ∈ {v}ᶜ
case h
ι : Sort ?u.140009
𝕜 : Type ?u.140012
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
G : SimpleGraph V
v w : V
⊢ w ∈ neighborSet G v ∪ neighborSet (Gᶜ) v ↔ w ∈ {v}ᶜ
have h := @ne_of_adj _ G
case h
ι : Sort ?u.140009
𝕜 : Type ?u.140012
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
G : SimpleGraph V
v w : V
h : ∀ {a b : V}, Adj G a b → a ≠ b
⊢ Adj G v w ∨ v ≠ w ∧ ¬Adj G v w ↔ ¬w = v
case h
ι : Sort ?u.140009
𝕜 : Type ?u.140012
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
G : SimpleGraph V
v w : V
h : ∀ {a b : V}, Adj G a b → a ≠ b
⊢ w ∈ neighborSet G v ∪ neighborSet (Gᶜ) v ↔ w ∈ {v}ᶜ
simp_rw [Set.mem_union, mem_neighborSet, compl_adj, Set.mem_compl_iff, Set.mem_singleton_iff]
no goals
case h
ι : Sort ?u.140009
𝕜 : Type ?u.140012
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
G : SimpleGraph V
v w : V
h : ∀ {a b : V}, Adj G a b → a ≠ b
⊢ Adj G v w ∨ v ≠ w ∧ ¬Adj G v w ↔ ¬w = v
tauto