F : Type ?u.404604
α : Type u_1
β : Type ?u.404610
γ : Type ?u.404613
ι : Type ?u.404616
κ : Type ?u.404619
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
his : IsGLB (↑s) i
⊢ IsLeast (↑s) i
F : Type ?u.404604
α : Type u_1
β : Type ?u.404610
γ : Type ?u.404613
ι : Type ?u.404616
κ : Type ?u.404619
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
⊢ IsGLB (↑s) i ↔ IsLeast (↑s) i
refine' ⟨fun his => _, IsLeast.isGLB⟩
F : Type ?u.404604
α : Type u_1
β : Type ?u.404610
γ : Type ?u.404613
ι : Type ?u.404616
κ : Type ?u.404619
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
his : IsGLB (↑s) i
⊢ i = min' s hs
F : Type ?u.404604
α : Type u_1
β : Type ?u.404610
γ : Type ?u.404613
ι : Type ?u.404616
κ : Type ?u.404619
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
his : IsGLB (↑s) i
⊢ IsLeast (↑s) i
suffices i = min' s hs by
  rw [this]
  exact isLeast_min' s hs
F : Type ?u.404604
α : Type u_1
β : Type ?u.404610
γ : Type ?u.404613
ι : Type ?u.404616
κ : Type ?u.404619
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
his : (∀ (x : α), x ∈ ↑s → i ≤ x) ∧ ∀ (x : α), x ∈ lowerBounds ↑s → x ≤ i
⊢ i = min' s hs
F : Type ?u.404604
α : Type u_1
β : Type ?u.404610
γ : Type ?u.404613
ι : Type ?u.404616
κ : Type ?u.404619
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
his : IsGLB (↑s) i
⊢ i = min' s hs
rw [IsGLB, IsGreatest, mem_lowerBounds, mem_upperBounds] at his
no goals
F : Type ?u.404604
α : Type u_1
β : Type ?u.404610
γ : Type ?u.404613
ι : Type ?u.404616
κ : Type ?u.404619
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
his : (∀ (x : α), x ∈ ↑s → i ≤ x) ∧ ∀ (x : α), x ∈ lowerBounds ↑s → x ≤ i
⊢ i = min' s hs
exact le_antisymm (his.1 (Finset.min' s hs) (Finset.min'_mem s hs)) (his.2 _ (Finset.min'_le s))
F : Type ?u.404604
α : Type u_1
β : Type ?u.404610
γ : Type ?u.404613
ι : Type ?u.404616
κ : Type ?u.404619
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
his : IsGLB (↑s) i
this : i = min' s hs
⊢ IsLeast (↑s) (min' s hs)
F : Type ?u.404604
α : Type u_1
β : Type ?u.404610
γ : Type ?u.404613
ι : Type ?u.404616
κ : Type ?u.404619
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
his : IsGLB (↑s) i
this : i = min' s hs
⊢ IsLeast (↑s) i
rw [this]
no goals
F : Type ?u.404604
α : Type u_1
β : Type ?u.404610
γ : Type ?u.404613
ι : Type ?u.404616
κ : Type ?u.404619
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
his : IsGLB (↑s) i
this : i = min' s hs
⊢ IsLeast (↑s) (min' s hs)
exact isLeast_min' s hs