Lemmas relating fintypes and order/lattice structure.

theorem Finset.sup_univ_eq_iSup {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [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_2} [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_2} [Fintype α] [SemilatticeSup α] [OrderTop α] (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} [Fintype α] [DecidableEq α] {s : Finset ι} {f : ι → Finset α} {a : α} : a ∈ Finset.inf s f ↔ ∀ i ∈ s, a ∈ f i

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

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