F : Type ?u.304015
α : Type u_1
β : Type ?u.304021
γ : Type ?u.304024
ι : Type u_2
κ : Type ?u.304030
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f : ι → α
a : α
⊢ (∀ (b : ι), b ∈ s → (WithBot.some ∘ f) b < ↑a) ↔ ∀ (i : ι), i ∈ s → f i < a
F : Type ?u.304015
α : Type u_1
β : Type ?u.304021
γ : Type ?u.304024
ι : Type u_2
κ : Type ?u.304030
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f : ι → α
a : α
⊢ sup' s H f < a ↔ ∀ (i : ι), i ∈ s → f i < a
rw [← WithBot.coe_lt_coe, coe_sup', Finset.sup_lt_iff (WithBot.bot_lt_coe a)]
no goals
F : Type ?u.304015
α : Type u_1
β : Type ?u.304021
γ : Type ?u.304024
ι : Type u_2
κ : Type ?u.304030
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f : ι → α
a : α
⊢ (∀ (b : ι), b ∈ s → (WithBot.some ∘ f) b < ↑a) ↔ ∀ (i : ι), i ∈ s → f i < a
exact ball_congr (fun _ _ => WithBot.coe_lt_coe)