mathlib documentation

order.partial_sups

The monotone sequence of partial supremums of a sequence #

We define partial_sups : (ℕ → α) → ℕ →ₘ α 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 nf 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_bot α] (f : → α) (n : ) :
theorem partial_sups_disjoint_of_disjoint {α : Type u_1} [distrib_lattice_bot α] (f : → α) (h : pairwise (disjoint on f)) {m n : } (hmn : m < 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