case intro
ι : Sort ?u.290851
𝕜 : Type ?u.290854
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w : V
e : Sym2 V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
t : ℕ
ht : Finset.min (image (fun v => degree G v) univ) = ↑t
⊢ minDegree G ≤ degree G v
ι : Sort ?u.290851
𝕜 : Type ?u.290854
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w : V
e : Sym2 V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
⊢ minDegree G ≤ degree G v
obtain ⟨t, ht⟩ := Finset.min_of_mem (mem_image_of_mem (fun v => G.degree v) (mem_univ v))
case intro
ι : Sort ?u.290851
𝕜 : Type ?u.290854
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w : V
e : Sym2 V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
t : ℕ
ht : Finset.min (image (fun v => degree G v) univ) = ↑t
this : t ≤ degree G v
⊢ minDegree G ≤ degree G v
case intro
ι : Sort ?u.290851
𝕜 : Type ?u.290854
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w : V
e : Sym2 V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
t : ℕ
ht : Finset.min (image (fun v => degree G v) univ) = ↑t
⊢ minDegree G ≤ degree G v
have := Finset.min_le_of_eq (mem_image_of_mem _ (mem_univ v)) ht
no goals
case intro
ι : Sort ?u.290851
𝕜 : Type ?u.290854
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w : V
e : Sym2 V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
t : ℕ
ht : Finset.min (image (fun v => degree G v) univ) = ↑t
this : t ≤ degree G v
⊢ minDegree G ≤ degree G v
rwa [minDegree, ht]