mathlib documentation

data.fintype.lattice

Lemmas relating fintypes and order/lattice structure. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem finset.sup_univ_eq_supr {α : Type u_1} {β : Type u_2} [fintype α] [complete_lattice β] (f : α β) :

A special case of finset.sup_eq_supr that omits the useless x ∈ univ binder.

theorem finset.inf_univ_eq_infi {α : Type u_1} {β : Type u_2} [fintype α] [complete_lattice β] (f : α β) :

A special case of finset.inf_eq_infi that omits the useless x ∈ univ binder.

@[simp]
theorem finset.fold_inf_univ {α : Type u_1} [fintype α] [semilattice_inf α] [order_bot α] (a : α) :
@[simp]
theorem finset.fold_sup_univ {α : Type u_1} [fintype α] [semilattice_sup α] [order_top α] (a : α) :
theorem finite.exists_max {α : Type u_1} {β : Type u_2} [finite α] [nonempty α] [linear_order β] (f : α β) :
(x₀ : α), (x : α), f x f x₀
theorem finite.exists_min {α : Type u_1} {β : Type u_2} [finite α] [nonempty α] [linear_order β] (f : α β) :
(x₀ : α), (x : α), f x₀ f x