# Lemmas relating fintypes and order/lattice structure. #

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

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

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

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

source
@[simp]
theorem Finset.fold_inf_univ {α : Type u_2} [Fintype α] [SemilatticeInf α] [OrderBot α] (a : α) :
fold min a (fun (x : α) => x) univ = ⊥
source
@[simp]
theorem Finset.fold_sup_univ {α : Type u_2} [Fintype α] [SemilatticeSup α] [OrderTop α] (a : α) :
fold max a (fun (x : α) => x) univ = ⊤
source
theorem Finset.mem_inf {ι : Type u_1} {α : Type u_2} [Fintype α] [DecidableEq α] {s : Finset ι} {f : ι → Finset α} {a : α} :
a ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i
source
theorem Finite.exists_max {α : Type u_2} {β : Type u_3} [Finite α] [Nonempty α] [LinearOrder β] (f : α → β) :
∃ (x₀ : α), ∀ (x : α), f x ≤ f x₀
source
theorem Finite.exists_min {α : Type u_2} {β : Type u_3} [Finite α] [Nonempty α] [LinearOrder β] (f : α → β) :
∃ (x₀ : α), ∀ (x : α), f x₀ ≤ f x