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