ι : Sort ?u.139320
𝕜 : Type ?u.139323
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 ⊆ ∅
ι : Sort ?u.139320
𝕜 : Type ?u.139323
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
⊢ Disjoint (neighborSet G v) (neighborSet (Gᶜ) v)
rw [Set.disjoint_iff]
case intro
ι : Sort ?u.139320
𝕜 : Type ?u.139323
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 : w ∈ neighborSet G v
h' : w ∈ neighborSet (Gᶜ) v
⊢ w ∈ ∅
ι : Sort ?u.139320
𝕜 : Type ?u.139323
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 ⊆ ∅
rintro w ⟨h, h'⟩
case intro
ι : Sort ?u.139320
𝕜 : Type ?u.139323
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 : w ∈ neighborSet G v
h' : v ≠ w ∧ ¬Adj G v w
⊢ w ∈ ∅
case intro
ι : Sort ?u.139320
𝕜 : Type ?u.139323
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 : w ∈ neighborSet G v
h' : w ∈ neighborSet (Gᶜ) v
⊢ w ∈ ∅
rw [mem_neighborSet, compl_adj] at h'
no goals
case intro
ι : Sort ?u.139320
𝕜 : Type ?u.139323
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 : w ∈ neighborSet G v
h' : v ≠ w ∧ ¬Adj G v w
⊢ w ∈ ∅
exact h'.2 h