V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
_h : v ≠ w
⊢ filter (fun x => x ∈ commonNeighbors ⊥ v w) univ = ∅
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
_h : v ≠ w
⊢ ¬Adj ⊥ v w → Fintype.card ↑(commonNeighbors ⊥ v w) = 0
simp only [card_eq_zero, Fintype.card_ofFinset, forall_true_left, not_false_iff, bot_adj]
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
_h : v ≠ w
a✝ : V
⊢ a✝ ∈ filter (fun x => x ∈ commonNeighbors ⊥ v w) univ ↔ a✝ ∈ ∅
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
_h : v ≠ w
⊢ filter (fun x => x ∈ commonNeighbors ⊥ v w) univ = ∅
ext
no goals
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
_h : v ≠ w
a✝ : V
⊢ a✝ ∈ filter (fun x => x ∈ commonNeighbors ⊥ v w) univ ↔ a✝ ∈ ∅
simp [mem_commonNeighbors]