# mathlib3documentation

order.partial_sups

# The monotone sequence of partial supremums of a sequence #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define partial_sups : (ℕ → α) → ℕ →o α inductively. For f : ℕ → α, partial_sups 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 conditionally_complete_lattices).
• 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 partial_sups_eq_bsupr, partial_sups_eq_sup_range, partial_sups_eq_sup'_range and 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.
• λ 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 partial_sups.gi.

## TODO #

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

def partial_sups {α : Type u_1} (f : α) :

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

Equations
@[simp]
theorem partial_sups_zero {α : Type u_1} (f : α) :
(partial_sups f) 0 = f 0
@[simp]
theorem partial_sups_succ {α : Type u_1} (f : α) (n : ) :
(partial_sups f) (n + 1) = (partial_sups f) n f (n + 1)
theorem le_partial_sups_of_le {α : Type u_1} (f : α) {m n : } (h : m n) :
theorem le_partial_sups {α : Type u_1} (f : α) :
theorem partial_sups_le {α : Type u_1} (f : α) (n : ) (a : α) (w : (m : ), m n f m a) :
@[simp]
theorem bdd_above_range_partial_sups {α : Type u_1} {f : α} :
theorem monotone.partial_sups_eq {α : Type u_1} {f : α} (hf : monotone f) :
theorem partial_sups_mono {α : Type u_1}  :
def partial_sups.gi {α : Type u_1}  :

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

Equations
theorem partial_sups_eq_sup'_range {α : Type u_1} (f : α) (n : ) :
(partial_sups f) n = (finset.range (n + 1)).sup' _ f
theorem partial_sups_eq_sup_range {α : Type u_1} [order_bot α] (f : α) (n : ) :
theorem partial_sups_disjoint_of_disjoint {α : Type u_1} [order_bot α] (f : α) (h : pairwise (disjoint on f)) {m n : } (hmn : m < n) :
theorem partial_sups_eq_csupr_Iic {α : Type u_1} (f : α) (n : ) :
(partial_sups f) n = (i : (set.Iic n)), f i
@[simp]
theorem csupr_partial_sups_eq {α : Type u_1} {f : α} (h : bdd_above (set.range f)) :
( (n : ), (partial_sups f) n) = (n : ), f n
theorem partial_sups_eq_bsupr {α : Type u_1} (f : α) (n : ) :
(partial_sups f) n = (i : ) (H : i n), f i
@[simp]
theorem supr_partial_sups_eq {α : Type u_1} (f : α) :
( (n : ), (partial_sups f) n) = (n : ), f n
theorem supr_le_supr_of_partial_sups_le_partial_sups {α : Type u_1} {f g : α} (h : ) :
( (n : ), f n) (n : ), g n
theorem supr_eq_supr_of_partial_sups_eq_partial_sups {α : Type u_1} {f g : α} (h : = ) :
( (n : ), f n) = (n : ), g n