Lemmas relating fintypes and order/lattice structure.

theorem Finset.sup_univ_eq_iSup {α : Type u_1} {β : Type u_2} [Fintype α] [CompleteLattice β] (f : α → β) : Finset.sup Finset.univ 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_1} {β : Type u_2} [Fintype α] [CompleteLattice β] (f : α → β) : Finset.inf Finset.univ 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_1} [Fintype α] [SemilatticeInf α] [OrderBot α] (a : α) : Finset.fold (fun x x_1 => x ⊓ x_1) a (fun x => x) Finset.univ = ⊥

@[simp]

theorem Finset.fold_sup_univ {α : Type u_1} [Fintype α] [SemilatticeSup α] [OrderTop α] (a : α) : Finset.fold (fun x x_1 => x ⊔ x_1) a (fun x => x) Finset.univ = ⊤

theorem Finite.exists_max {α : Type u_1} {β : Type u_2} [Finite α] [Nonempty α] [LinearOrder β] (f : α → β) : ∃ x₀, ∀ (x : α), f x ≤ f x₀

theorem Finite.exists_min {α : Type u_1} {β : Type u_2} [Finite α] [Nonempty α] [LinearOrder β] (f : α → β) : ∃ x₀, ∀ (x : α), f x₀ ≤ f x