theorem Finset.sup_eq_iSup' {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrderBot β] (s : Finset α) (f : α → β) : s.sup f = ⨆ a ∈ s, f a