# The monotone sequence of partial supremums of a sequence #

We define partialSups : (ℕ → α) → ℕ →o α inductively. For f : ℕ → α, partialSups f is the sequence f 0, f 0 ⊔ f 1, f 0 ⊔ f 1 ⊔ f 2, ... The point of this definition is that

• it doesn't need a ⨆, as opposed to ⨆ (i ≤ n), f i (which also means the wrong thing on ConditionallyCompleteLattices).
• it doesn't need a ⊥, as opposed to (Finset.range (n + 1)).sup f.
• it avoids needing to prove that Finset.range (n + 1) is nonempty to use Finset.sup'.

Equivalence with those definitions is shown by partialSups_eq_biSup, partialSups_eq_sup_range, and partialSups_eq_sup'_range respectively.

## Notes #

One might dispute whether this sequence should start at f 0 or ⊥. We choose the former because :

• Starting at ⊥ requires... having a bottom element.
• fun f n ↦ (Finset.range n).sup f is already effectively the sequence starting at ⊥.
• If we started at ⊥ we wouldn't have the Galois insertion. See partialSups.gi.

## TODO #

One could generalize partialSups to any locally finite bot preorder domain, in place of ℕ. Necessary for the TODO in the module docstring of Order.disjointed.

def partialSups {α : Type u_1} [] (f : α) :

The monotone sequence whose value at n is the supremum of the f m where m ≤ n.

Equations
• = { toFun := Nat.rec (f 0) fun (n : ) (a : α) => a f (n + 1), monotone' := }
Instances For
@[simp]
theorem partialSups_zero {α : Type u_1} [] (f : α) :
() 0 = f 0
@[simp]
theorem partialSups_succ {α : Type u_1} [] (f : α) (n : ) :
() (n + 1) = () n f (n + 1)
theorem partialSups_iff_forall {α : Type u_1} [] {f : α} (p : αProp) (hp : ∀ {a b : α}, p (a b) p a p b) {n : } :
p (() n) kn, p (f k)
@[simp]
theorem partialSups_le_iff {α : Type u_1} [] {f : α} {n : } {a : α} :
() n a kn, f k a
theorem le_partialSups_of_le {α : Type u_1} [] (f : α) {m : } {n : } (h : m n) :
f m () n
theorem le_partialSups {α : Type u_1} [] (f : α) :
f ()
theorem partialSups_le {α : Type u_1} [] (f : α) (n : ) (a : α) (w : mn, f m a) :
() n a
@[simp]
theorem upperBounds_range_partialSups {α : Type u_1} [] (f : α) :
@[simp]
theorem bddAbove_range_partialSups {α : Type u_1} [] {f : α} :
theorem Monotone.partialSups_eq {α : Type u_1} [] {f : α} (hf : ) :
() = f
theorem partialSups_mono {α : Type u_1} [] :
Monotone partialSups
def partialSups.gi {α : Type u_1} [] :
GaloisInsertion partialSups DFunLike.coe

partialSups forms a Galois insertion with the coercion from monotone functions to functions.

Equations
• partialSups.gi = { choice := fun (f : α) (h : () f) => { toFun := f, monotone' := }, gc := , le_l_u := , choice_eq := }
Instances For
theorem partialSups_eq_sup'_range {α : Type u_1} [] (f : α) (n : ) :
() n = (Finset.range (n + 1)).sup' f
theorem partialSups_apply {ι : Type u_2} {π : ιType u_3} [(i : ι) → SemilatticeSup (π i)] (f : (i : ι) → π i) (n : ) (i : ι) :
() n i = (partialSups fun (x : ) => f x i) n
theorem partialSups_eq_sup_range {α : Type u_1} [] [] (f : α) (n : ) :
() n = (Finset.range (n + 1)).sup f
@[simp]
theorem disjoint_partialSups_left {α : Type u_1} [] [] {f : α} {n : } {x : α} :
Disjoint (() n) x kn, Disjoint (f k) x
@[simp]
theorem disjoint_partialSups_right {α : Type u_1} [] [] {f : α} {n : } {x : α} :
Disjoint x (() n) kn, Disjoint x (f k)
theorem partialSups_disjoint_of_disjoint {α : Type u_1} [] [] (f : α) (h : Pairwise (Disjoint on f)) {m : } {n : } (hmn : m < n) :
Disjoint (() m) (f n)
theorem partialSups_eq_ciSup_Iic {α : Type u_1} (f : α) (n : ) :
() n = ⨆ (i : ()), f i
@[simp]
theorem ciSup_partialSups_eq {α : Type u_1} {f : α} (h : ) :
⨆ (n : ), () n = ⨆ (n : ), f n
theorem partialSups_eq_biSup {α : Type u_1} [] (f : α) (n : ) :
() n = ⨆ (i : ), ⨆ (_ : i n), f i
theorem iSup_partialSups_eq {α : Type u_1} [] (f : α) :
⨆ (n : ), () n = ⨆ (n : ), f n
theorem iSup_le_iSup_of_partialSups_le_partialSups {α : Type u_1} [] {f : α} {g : α} (h : ) :
⨆ (n : ), f n ⨆ (n : ), g n
theorem iSup_eq_iSup_of_partialSups_eq_partialSups {α : Type u_1} [] {f : α} {g : α} (h : ) :
⨆ (n : ), f n = ⨆ (n : ), g n