Documentation

Mathlib.Data.Fintype.Lattice

Lemmas relating fintypes and order/lattice structure. #

theorem Finset.sup_univ_eq_supᵢ {α : Type u_2} {β : Type u_1} [inst : Fintype α] [inst : CompleteLattice β] (f : αβ) :
Finset.sup Finset.univ f = supᵢ f

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

theorem Finset.inf_univ_eq_infᵢ {α : Type u_2} {β : Type u_1} [inst : Fintype α] [inst : CompleteLattice β] (f : αβ) :
Finset.inf Finset.univ f = infᵢ f

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

@[simp]
theorem Finset.fold_inf_univ {α : Type u_1} [inst : Fintype α] [inst : SemilatticeInf α] [inst : 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} [inst : Fintype α] [inst : SemilatticeSup α] [inst : 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} [inst : Finite α] [inst : Nonempty α] [inst : LinearOrder β] (f : αβ) :
x₀, ∀ (x : α), f x f x₀
theorem Finite.exists_min {α : Type u_1} {β : Type u_2} [inst : Finite α] [inst : Nonempty α] [inst : LinearOrder β] (f : αβ) :
x₀, ∀ (x : α), f x₀ f x