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 : α → β) :
finset.univ.sup f = supr 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 : α → β) :
finset.univ.inf f = infi 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 : α) :
finset.fold has_inf.inf a (λ (x : α), x) finset.univ = ⊥
@[simp]
theorem
finset.fold_sup_univ
{α : Type u_1}
[fintype α]
[semilattice_sup α]
[order_top α]
(a : α) :
finset.fold has_sup.sup a (λ (x : α), x) finset.univ = ⊤