Finset.sup_univ_eq_iSup
theorem Finset.sup_univ_eq_iSup :
∀ {α : Type u_2} {β : Type u_3} [inst : Fintype α] [inst_1 : CompleteLattice β] (f : α → β),
Finset.univ.sup f = iSup f
The theorem `Finset.sup_univ_eq_iSup` states that for every function `f` from a type `α` to a type `β`, where `α` is a finite type and `β` is a complete lattice, the supremum of the function `f` over the universal set of `α` (i.e., `Finset.sup Finset.univ f`) is equal to the indexed supremum of the function `f` (i.e., `iSup f`). In terms of set theory, it means that taking the supremum of `f` over all elements of `α` (since `Finset.univ` contains all elements of `α`) is equivalent to taking the supremum of `f` over its range.
More concisely: For a function `f` from a finite type `α` to a complete lattice `β`, `Finset.sup Finset.univ f` equals `iSup f`.
|
Finset.inf_univ_eq_iInf
theorem Finset.inf_univ_eq_iInf :
∀ {α : Type u_2} {β : Type u_3} [inst : Fintype α] [inst_1 : CompleteLattice β] (f : α → β),
Finset.univ.inf f = iInf f
This theorem states that, for any finite type `α` and any type `β` forming a complete lattice, the function `f : α → β` when applied to the universal finite set (Finset.univ) of type `α` and then finding the infimum (Finset.univ.inf f), is equivalent to finding the indexed infimum (iInf f) of the function `f`. Essentially, it establishes a link between the operation of finding the infimum on a finite set and finding the indexed infimum on a function for any pair of types where one is finite and the other forms a complete lattice.
More concisely: For any finite type `α` and complete lattice `β`, the function `f : α → β` applied to the universal finite set of `α` and finding its infimum is equivalent to computing the indexed infimum of `f`.
|