# Lemmas relating fintypes and order/lattice structure. #

theorem Finset.sup_univ_eq_iSup {α : Type u_2} {β : Type u_3} [] [] (f : αβ) :
Finset.univ.sup f = iSup f

A special case of Finset.sup_eq_iSup that omits the useless x ∈ univ binder.

theorem Finset.inf_univ_eq_iInf {α : Type u_2} {β : Type u_3} [] [] (f : αβ) :
Finset.univ.inf f = iInf f

A special case of Finset.inf_eq_iInf that omits the useless x ∈ univ binder.

@[simp]
theorem Finset.fold_inf_univ {α : Type u_2} [] [] [] (a : α) :
Finset.fold (fun (x x_1 : α) => x x_1) a (fun (x : α) => x) Finset.univ =
@[simp]
theorem Finset.fold_sup_univ {α : Type u_2} [] [] [] (a : α) :
Finset.fold (fun (x x_1 : α) => x x_1) a (fun (x : α) => x) Finset.univ =
theorem Finset.mem_inf {ι : Type u_1} {α : Type u_2} [] [] {s : } {f : ι} {a : α} :
a s.inf f is, a f i
theorem Finite.exists_max {α : Type u_2} {β : Type u_3} [] [] [] (f : αβ) :
∃ (x₀ : α), ∀ (x : α), f x f x₀
theorem Finite.exists_min {α : Type u_2} {β : Type u_3} [] [] [] (f : αβ) :
∃ (x₀ : α), ∀ (x : α), f x₀ f x