ι : Sort ?u.206794
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : V
inst✝ : Fintype ↑(neighborSet G' v)
⊢ (∃! a, a ∈ Set.toFinset (neighborSet G' v)) ↔ ∃! w, Adj G' v w
ι : Sort ?u.206794
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : V
inst✝ : Fintype ↑(neighborSet G' v)
⊢ degree G' v = 1 ↔ ∃! w, Adj G' v w
rw [← finset_card_neighborSet_eq_degree, Finset.card_eq_one, Finset.singleton_iff_unique_mem]
no goals
ι : Sort ?u.206794
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : V
inst✝ : Fintype ↑(neighborSet G' v)
⊢ (∃! a, a ∈ Set.toFinset (neighborSet G' v)) ↔ ∃! w, Adj G' v w
simp only [Set.mem_toFinset, mem_neighborSet]