mathlib3 documentation

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

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 :

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} [semilattice_sup α] (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} [semilattice_sup α] (f : α) :
(partial_sups f) 0 = f 0
@[simp]
theorem partial_sups_succ {α : Type u_1} [semilattice_sup α] (f : α) (n : ) :
(partial_sups f) (n + 1) = (partial_sups f) n f (n + 1)
theorem le_partial_sups_of_le {α : Type u_1} [semilattice_sup α] (f : α) {m n : } (h : m n) :
theorem le_partial_sups {α : Type u_1} [semilattice_sup α] (f : α) :
theorem partial_sups_le {α : Type u_1} [semilattice_sup α] (f : α) (n : ) (a : α) (w : (m : ), m n f m a) :
theorem monotone.partial_sups_eq {α : Type u_1} [semilattice_sup α] {f : α} (hf : monotone f) :

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

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