Finset.sup'_eq_csSup_image
theorem Finset.sup'_eq_csSup_image :
∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLattice α] (s : Finset ι) (H : s.Nonempty) (f : ι → α),
s.sup' H f = sSup (f '' ↑s)
This theorem states that for any types `ι` and `α`, where `α` is a conditionally complete lattice, and any nonempty finite set `s` of type `ι`, and any function `f` from `ι` to `α`, the sup' of `s` under `f` is equal to the supremum (`sSup`) of the image of `s` under `f`. This means that the greatest element achieved by mapping the elements of the finite set `s` via the function `f` can also be obtained as the supremum of the image set of `s` under `f`.
More concisely: For any conditionally complete lattice `α`, function `f` from a nonempty finite type `ι` to `α`, and set `s` of type `ι`, the image of the supremum of `s` under `f` is equal to the supremum of the image of `s` under `f`. In other words, `sup (map f s) = sSup`.
|
Finset.inf'_eq_csInf_image
theorem Finset.inf'_eq_csInf_image :
∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLattice α] (s : Finset ι) (H : s.Nonempty) (f : ι → α),
s.inf' H f = sInf (f '' ↑s)
This theorem states that for any type `ι`, any type `α` which forms a conditionally complete lattice, any nonempty finite set `s` of type `ι`, and any function `f` from `ι` to `α`, the infimum of the image of `s` under `f` (as calculated by the method `Finset.inf'`) is equal to the supremum of the lower bounds (`sInf`) of the set of all images of the elements of `s` under `f`. In other words, the infimum of the set obtained by applying `f` to each element of `s` can be obtained by finding the supremum of all lower bounds of this set.
More concisely: For any nonempty finite set `s` and function `f` from a conditionally complete lattice `ι` to a lattice `α`, the infimum of `f`'s image of `s` equals the supremum of `f`'s lower bounds on `s`.
|