Documentation

Mathlib.Order.PartialSups

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

Equivalence with those definitions is shown by partialSups_eq_bsupᵢ, 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 :

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} [inst : SemilatticeSup α] (f : α) :

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

Equations
@[simp]
theorem partialSups_zero {α : Type u_1} [inst : SemilatticeSup α] (f : α) :
↑(partialSups f) 0 = f 0
@[simp]
theorem partialSups_succ {α : Type u_1} [inst : SemilatticeSup α] (f : α) (n : ) :
↑(partialSups f) (n + 1) = ↑(partialSups f) n f (n + 1)
theorem le_partialSups_of_le {α : Type u_1} [inst : SemilatticeSup α] (f : α) {m : } {n : } (h : m n) :
f m ↑(partialSups f) n
theorem le_partialSups {α : Type u_1} [inst : SemilatticeSup α] (f : α) :
f ↑(partialSups f)
theorem partialSups_le {α : Type u_1} [inst : SemilatticeSup α] (f : α) (n : ) (a : α) (w : ∀ (m : ), m nf m a) :
↑(partialSups f) n a
@[simp]
theorem bddAbove_range_partialSups {α : Type u_1} [inst : SemilatticeSup α] {f : α} :
theorem Monotone.partialSups_eq {α : Type u_1} [inst : SemilatticeSup α] {f : α} (hf : Monotone f) :
↑(partialSups f) = f
theorem partialSups_mono {α : Type u_1} [inst : SemilatticeSup α] :
Monotone partialSups
def partialSups.gi {α : Type u_1} [inst : SemilatticeSup α] :
GaloisInsertion partialSups OrderHom.toFun

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

Equations
  • One or more equations did not get rendered due to their size.
theorem partialSups_eq_sup'_range {α : Type u_1} [inst : SemilatticeSup α] (f : α) (n : ) :
↑(partialSups f) n = Finset.sup' (Finset.range (n + 1)) (_ : x, x Finset.range (n + 1)) f
theorem partialSups_eq_sup_range {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] (f : α) (n : ) :
theorem partialSups_disjoint_of_disjoint {α : Type u_1} [inst : DistribLattice α] [inst : OrderBot α] (f : α) (h : Pairwise (Disjoint on f)) {m : } {n : } (hmn : m < n) :
Disjoint (↑(partialSups f) m) (f n)
theorem partialSups_eq_csupᵢ_Iic {α : Type u_1} [inst : ConditionallyCompleteLattice α] (f : α) (n : ) :
↑(partialSups f) n = i, f i
@[simp]
theorem csupᵢ_partialSups_eq {α : Type u_1} [inst : ConditionallyCompleteLattice α] {f : α} (h : BddAbove (Set.range f)) :
(n, ↑(partialSups f) n) = n, f n
theorem partialSups_eq_bsupᵢ {α : Type u_1} [inst : CompleteLattice α] (f : α) (n : ) :
↑(partialSups f) n = i, h, f i
theorem supᵢ_partialSups_eq {α : Type u_1} [inst : CompleteLattice α] (f : α) :
(n, ↑(partialSups f) n) = n, f n
theorem supᵢ_le_supᵢ_of_partialSups_le_partialSups {α : Type u_1} [inst : CompleteLattice α] {f : α} {g : α} (h : partialSups f partialSups g) :
(n, f n) n, g n
theorem supᵢ_eq_supᵢ_of_partialSups_eq_partialSups {α : Type u_1} [inst : CompleteLattice α] {f : α} {g : α} (h : partialSups f = partialSups g) :
(n, f n) = n, g n