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_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 :

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

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

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

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

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