case h
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬Adj G a b
⊢ ¬e ∈ incidenceSet G a ∩ incidenceSet G b
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬Adj G a b
⊢ incMatrix R G a e * incMatrix R G b e = 0
rw [incMatrix_apply_mul_incMatrix_apply, Set.indicator_of_not_mem]
case h
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬Adj G a b
⊢ ¬e ∈ ∅
case h
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬Adj G a b
⊢ ¬e ∈ incidenceSet G a ∩ incidenceSet G b
rw [G.incidenceSet_inter_incidenceSet_of_not_adj h hab]
no goals
case h
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬Adj G a b
⊢ ¬e ∈ ∅
exact Set.not_mem_empty e