Documentation

Mathlib.Data.Fintype.Lattice

Lemmas relating fintypes and order/lattice structure. #

theorem Finset.sup_univ_eq_iSup {α : Type u_2} {β : Type u_3} [Fintype α] [CompleteLattice β] (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} [Fintype α] [CompleteLattice β] (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} [Fintype α] [SemilatticeInf α] [OrderBot α] (a : α) :
Finset.fold (fun (x1 x2 : α) => x1 x2) a (fun (x : α) => x) Finset.univ =
@[simp]
theorem Finset.fold_sup_univ {α : Type u_2} [Fintype α] [SemilatticeSup α] [OrderTop α] (a : α) :
Finset.fold (fun (x1 x2 : α) => x1 x2) a (fun (x : α) => x) Finset.univ =
theorem Finset.mem_inf {ι : Type u_1} {α : Type u_2} [Fintype α] [DecidableEq α] {s : Finset ι} {f : ιFinset α} {a : α} :
a s.inf f is, 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