V : Type u
G : SimpleGraph V
P : Partition G
v w : V
h : Adj G v w
hn : partOfVertex P v = partOfVertex P w
⊢ False
V : Type u
G : SimpleGraph V
P : Partition G
v w : V
h : Adj G v w
⊢ partOfVertex P v ≠ partOfVertex P w
intro hn
V : Type u
G : SimpleGraph V
P : Partition G
v w : V
h : Adj G v w
hn : partOfVertex P v = partOfVertex P w
hw : w ∈ partOfVertex P w
⊢ False
V : Type u
G : SimpleGraph V
P : Partition G
v w : V
h : Adj G v w
hn : partOfVertex P v = partOfVertex P w
⊢ False
have hw := P.mem_partOfVertex w
V : Type u
G : SimpleGraph V
P : Partition G
v w : V
h : Adj G v w
hn : partOfVertex P v = partOfVertex P w
hw : w ∈ partOfVertex P v
⊢ False
V : Type u
G : SimpleGraph V
P : Partition G
v w : V
h : Adj G v w
hn : partOfVertex P v = partOfVertex P w
hw : w ∈ partOfVertex P w
⊢ False
rw [← hn] at hw
no goals
V : Type u
G : SimpleGraph V
P : Partition G
v w : V
h : Adj G v w
hn : partOfVertex P v = partOfVertex P w
hw : w ∈ partOfVertex P v
⊢ False
exact P.independent _ (P.partOfVertex_mem v) (P.mem_partOfVertex v) hw (G.ne_of_adj h) h