ι : Sort ?u.200951
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)
inst✝ : Fintype ↑(SimpleGraph.neighborSet G v)
⊢ degree G' v ≤ Fintype.card ↑(SimpleGraph.neighborSet G v)
ι : Sort ?u.200951
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)
inst✝ : Fintype ↑(SimpleGraph.neighborSet G v)
⊢ degree G' v ≤ SimpleGraph.degree G v
rw [← card_neighborSet_eq_degree]
no goals
ι : Sort ?u.200951
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)
inst✝ : Fintype ↑(SimpleGraph.neighborSet G v)
⊢ degree G' v ≤ Fintype.card ↑(SimpleGraph.neighborSet G v)
exact Set.card_le_of_subset (G'.neighborSet_subset v)