theorem Finset.Nonempty.sSup_eq_max' {α : Type u_1} [CompleteLinearOrder α] {s : Finset α} (h : s.Nonempty) : sSup ↑s = s.max' h

theorem Finset.iSup_eq_max'_image {α : Type u_1} {ι : Type u_2} [CompleteLinearOrder α] (f : ι → α) {s : Finset ι} (h : s.Nonempty) (h' : (image f s).Nonempty := by simpa using h) : ⨆ i ∈ s, f i = (image f s).max' h'

theorem Finset.iInf_eq_min'_image {α : Type u_1} {ι : Type u_2} [CompleteLinearOrder α] (f : ι → α) {s : Finset ι} (h : s.Nonempty) (h' : (image f s).Nonempty := by simpa using h) : ⨅ i ∈ s, f i = (image f s).min' h'

theorem Finset.iInf_mem_image {α : Type u_1} {ι : Type u_2} [CompleteLinearOrder α] (f : ι → α) {s : Finset ι} (h : s.Nonempty) : ⨅ i ∈ s, f i ∈ image f s

theorem Set.Finite.iInf_mem_image {α : Type u_1} {ι : Type u_2} [CompleteLinearOrder α] (f : ι → α) {s : Set ι} (h : s.Nonempty) (hs : s.Finite) : ⨅ i ∈ s, f i ∈ f '' s

theorem Set.Finite.lt_iInf_iff {α : Type u_1} {ι : Type u_2} [CompleteLinearOrder α] {s : Set ι} {f : ι → α} (h : s.Nonempty) (hs : s.Finite) {a : α} : a < ⨅ i ∈ s, f i ↔ ∀ x ∈ s, a < f x