doc-next-gen

Mathlib.Order.PartialSups

Module docstring

{"# The monotone sequence of partial supremums of a sequence

For ι a preorder in which all bounded-above intervals are finite (such as ℕ), and α a ⊔-semilattice, we define partialSups : (ι → α) → ι →o α by the formula partialSups f i = (Finset.Iic i).sup' ⋯ f, where the ⋯ denotes a proof that Finset.Iic i is nonempty. This is a way of spelling ⊔ k ≤ i, f k which does not require a α to have a bottom element, and makes sense in conditionally-complete lattices (where indexed suprema over sets are badly-behaved).

Under stronger hypotheses on α and ι, we show that this coincides with other candidate definitions, see e.g. partialSups_eq_biSup, partialSups_eq_sup_range, and partialSups_eq_sup'_range.

We show this construction gives a Galois insertion between functions ι → α and monotone functions ι →o α, see partialSups.gi.

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. * fun f i ↦ (Finset.Iio i).sup f is already effectively the sequence starting at ⊥. * If we started at ⊥ we wouldn't have the Galois insertion. See partialSups.gi.

","### Functions out of ℕ ","### Functions valued in a distributive lattice

These lemmas require the target to be a distributive lattice, so they are not useful (or true) in situations such as submodules. ","### Lemmas about the supremum over the whole domain

These lemmas require some completeness assumptions on the target space. ","### Functions into Set α "}

partialSups definition
(f : ι → α) : ι →o α
Full source 
/-- The monotone sequence whose value at `i` is the supremum of the `f j` where `j ≤ i`. -/
def partialSups (f : ι → α) : ι →o α where
  toFun i := (Iic i).sup' nonempty_Iic f
  monotone' _ _ hmn := sup'_mono f (Iic_subset_Iic.mpr hmn) nonempty_Iic
Monotone sequence of partial suprema
Informal description
Given a preorder $\iota$ where all bounded-above intervals are finite (such as $\mathbb{N}$) and a join-semilattice $\alpha$, the function `partialSups` maps a sequence $f : \iota \to \alpha$ to a monotone sequence $\iota \to \alpha$ where the value at each $i \in \iota$ is the supremum of $\{f(j) \mid j \leq i\}$. More precisely, for each $i \in \iota$, the value $\text{partialSups}(f)(i)$ is defined as $\bigsqcup_{j \leq i} f(j)$, computed as the supremum over the finite set $\text{Iic}(i) = \{j \in \iota \mid j \leq i\}$.
partialSups_apply theorem
(f : ι → α) (i : ι) : partialSups f i = (Iic i).sup' nonempty_Iic f
Full source 
lemma partialSups_apply (f : ι → α) (i : ι) :
    partialSups f i = (Iic i).sup' nonempty_Iic f :=
  rfl
Partial Suprema as Supremum over Lower-Closed Interval
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite (e.g., $\mathbb{N}$), and let $\alpha$ be a join-semilattice. For any function $f : \iota \to \alpha$ and any element $i \in \iota$, the value of the partial suprema function at $i$ is equal to the supremum of $f$ over the lower-closed interval $\text{Iic}(i) = \{j \in \iota \mid j \leq i\}$. That is, \[ \text{partialSups}(f)(i) = \bigsqcup_{j \leq i} f(j). \]
partialSups_iff_forall theorem
{f : ι → α} (p : α → Prop) (hp : ∀ {a b}, p (a ⊔ b) ↔ p a ∧ p b) {i : ι} : p (partialSups f i) ↔ ∀ j ≤ i, p (f j)
Full source 
lemma partialSups_iff_forall {f : ι → α} (p : α → Prop)
    (hp : ∀ {a b}, p (a ⊔ b) ↔ p a ∧ p b) {i : ι} :
    p (partialSups f i) ↔ ∀ j ≤ i, p (f j) := by
  classical
  rw [partialSups_apply, comp_sup'_eq_sup'_comp (γ := Propᵒᵈ) _ p, sup'_eq_sup]
  · show (Iic i).inf (p ∘ f) ↔ _
    simp [Finset.inf_eq_iInf]
  · intro x y
    rw [hp]
    rfl
Characterization of Predicate on Partial Suprema via Pointwise Condition
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite (e.g., $\mathbb{N}$), and let $\alpha$ be a join-semilattice. Given a function $f : \iota \to \alpha$ and a predicate $p : \alpha \to \mathrm{Prop}$ such that for any $a, b \in \alpha$, $p(a \sqcup b)$ holds if and only if both $p(a)$ and $p(b)$ hold, then for any $i \in \iota$, the predicate $p$ holds at the partial supremum $\mathrm{partialSups}(f)(i)$ if and only if $p$ holds at $f(j)$ for all $j \leq i$. In other words: \[ p\left(\bigsqcup_{j \leq i} f(j)\right) \leftrightarrow \forall j \leq i, p(f(j)). \]
partialSups_le_iff theorem
{f : ι → α} {i : ι} {a : α} : partialSups f i ≤ a ↔ ∀ j ≤ i, f j ≤ a
Full source 
@[simp]
lemma partialSups_le_iff {f : ι → α} {i : ι} {a : α} :
    partialSupspartialSups f i ≤ a ↔ ∀ j ≤ i, f j ≤ a :=
  partialSups_iff_forall (· ≤ a) sup_le_iff
Supremum Bound Criterion for Partial Suprema: $\bigsqcup_{j \leq i} f(j) \leq a \leftrightarrow \forall j \leq i, f(j) \leq a$
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite (e.g., $\mathbb{N}$), and let $\alpha$ be a join-semilattice. For any function $f : \iota \to \alpha$, any element $i \in \iota$, and any $a \in \alpha$, the partial supremum $\mathrm{partialSups}(f)(i)$ is less than or equal to $a$ if and only if $f(j) \leq a$ for all $j \leq i$. In other words: \[ \bigsqcup_{j \leq i} f(j) \leq a \leftrightarrow \forall j \leq i, f(j) \leq a. \]
le_partialSups_of_le theorem
(f : ι → α) {i j : ι} (h : i ≤ j) : f i ≤ partialSups f j
Full source 
theorem le_partialSups_of_le (f : ι → α) {i j : ι} (h : i ≤ j) :
    f i ≤ partialSups f j :=
  partialSups_le_iff.1 le_rfl i h
Monotonicity of Partial Suprema: $f(i) \leq \bigsqcup_{k \leq j} f(k)$ for $i \leq j$
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite (e.g., $\mathbb{N}$), and let $\alpha$ be a join-semilattice. For any function $f : \iota \to \alpha$ and any elements $i, j \in \iota$ such that $i \leq j$, the value $f(i)$ is less than or equal to the partial supremum $\mathrm{partialSups}(f)(j) = \bigsqcup_{k \leq j} f(k)$. In other words: \[ i \leq j \implies f(i) \leq \bigsqcup_{k \leq j} f(k). \]
le_partialSups theorem
(f : ι → α) : f ≤ partialSups f
Full source 
theorem le_partialSups (f : ι → α) :
    f ≤ partialSups f :=
  fun _ => le_partialSups_of_le f le_rfl
Pointwise Inequality Between Function and Its Partial Suprema
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite (e.g., $\mathbb{N}$), and let $\alpha$ be a join-semilattice. For any function $f : \iota \to \alpha$, the function $f$ is pointwise less than or equal to its partial suprema function $\mathrm{partialSups}(f)$, i.e., for every $i \in \iota$, we have $f(i) \leq \mathrm{partialSups}(f)(i) = \bigsqcup_{j \leq i} f(j)$. In other words: \[ \forall i \in \iota, \quad f(i) \leq \bigsqcup_{j \leq i} f(j). \]
partialSups_le theorem
(f : ι → α) (i : ι) (a : α) (w : ∀ j ≤ i, f j ≤ a) : partialSups f i ≤ a
Full source 
theorem partialSups_le (f : ι → α) (i : ι) (a : α) (w : ∀ j ≤ i, f j ≤ a) :
    partialSups f i ≤ a :=
  partialSups_le_iff.2 w
Partial Supremum Bound: $\bigsqcup_{j \leq i} f(j) \leq a$ when $f(j) \leq a$ for all $j \leq i$
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite (e.g., $\mathbb{N}$), and let $\alpha$ be a join-semilattice. For any function $f : \iota \to \alpha$, any $i \in \iota$, and any $a \in \alpha$, if $f(j) \leq a$ for all $j \leq i$, then the partial supremum $\bigsqcup_{j \leq i} f(j) \leq a$.
upperBounds_range_partialSups theorem
(f : ι → α) : upperBounds (Set.range (partialSups f)) = upperBounds (Set.range f)
Full source 
@[simp]
lemma upperBounds_range_partialSups (f : ι → α) :
    upperBounds (Set.range (partialSups f)) = upperBounds (Set.range f) := by
  ext a
  simp only [mem_upperBounds, Set.forall_mem_range, partialSups_le_iff]
  exact ⟨fun h _ ↦ h _ _ le_rfl, fun h _ _ _ ↦ h _⟩
Equality of Upper Bounds for Partial Suprema and Original Function
Informal description
For any function $f : \iota \to \alpha$ from a preorder $\iota$ (where all bounded-above intervals are finite) to a join-semilattice $\alpha$, the set of upper bounds of the range of the partial suprema function $\text{partialSups}(f)$ is equal to the set of upper bounds of the range of $f$ itself. In other words, an element $a \in \alpha$ is an upper bound for $\{\text{partialSups}(f)(i) \mid i \in \iota\}$ if and only if it is an upper bound for $\{f(i) \mid i \in \iota\}$.
bddAbove_range_partialSups theorem
{f : ι → α} : BddAbove (Set.range (partialSups f)) ↔ BddAbove (Set.range f)
Full source 
@[simp]
theorem bddAbove_range_partialSups {f : ι → α} :
    BddAboveBddAbove (Set.range (partialSups f)) ↔ BddAbove (Set.range f) :=
  .of_eq <| congr_arg Set.Nonempty <| upperBounds_range_partialSups f
Boundedness of Partial Suprema Range $\leftrightarrow$ Boundedness of Original Function Range
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite (such as $\mathbb{N}$), and let $\alpha$ be a join-semilattice. For any function $f : \iota \to \alpha$, the range of the partial suprema function $\text{partialSups}(f)$ is bounded above if and only if the range of $f$ is bounded above. In other words, there exists an upper bound for the set $\{\text{partialSups}(f)(i) \mid i \in \iota\}$ if and only if there exists an upper bound for the set $\{f(i) \mid i \in \iota\}$.
Monotone.partialSups_eq theorem
{f : ι → α} (hf : Monotone f) : partialSups f = f
Full source 
theorem Monotone.partialSups_eq {f : ι → α} (hf : Monotone f) :
    partialSups f = f :=
  funext fun i ↦ le_antisymm (partialSups_le _ _ _ (@hf · i)) (le_partialSups _ _)
Monotone Sequences Coincide with Their Partial Suprema
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite (e.g., $\mathbb{N}$), and let $\alpha$ be a join-semilattice. For any monotone function $f : \iota \to \alpha$, the sequence of partial suprema $\mathrm{partialSups}(f)$ coincides with $f$ itself, i.e., \[ \mathrm{partialSups}(f) = f. \] Here, $\mathrm{partialSups}(f)(i) = \bigsqcup_{j \leq i} f(j)$ for each $i \in \iota$.
partialSups_mono theorem
: Monotone (partialSups : (ι → α) → ι →o α)
Full source 
theorem partialSups_mono :
    Monotone (partialSups : (ι → α) → ι →o α) :=
  fun _ _ h _ ↦ partialSups_le_iff.2 fun j hj ↦ (h j).trans (le_partialSups_of_le _ hj)
Monotonicity of the Partial Suprema Operator: $f_1 \leq f_2 \implies \text{partialSups}(f_1) \leq \text{partialSups}(f_2)$
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite (such as $\mathbb{N}$), and let $\alpha$ be a join-semilattice. The function `partialSups` that maps a sequence $f : \iota \to \alpha$ to its sequence of partial suprema is monotone. That is, if $f_1 \leq f_2$ pointwise (i.e., $f_1(i) \leq f_2(i)$ for all $i \in \iota$), then the corresponding partial suprema sequences satisfy $\text{partialSups}(f_1) \leq \text{partialSups}(f_2)$ as order homomorphisms. In other words: \[ f_1 \leq f_2 \implies \text{partialSups}(f_1) \leq \text{partialSups}(f_2). \]
partialSups_monotone theorem
(f : ι → α) : Monotone (partialSups f)
Full source 
lemma partialSups_monotone (f : ι → α) :
    Monotone (partialSups f) :=
  fun i _ hnm ↦ partialSups_le f i _ (fun _ hm'n ↦ le_partialSups_of_le _ (hm'n.trans hnm))
Monotonicity of Partial Suprema Sequence: $\bigsqcup_{k \leq i} f(k) \leq \bigsqcup_{k \leq j} f(k)$ for $i \leq j$
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite (such as $\mathbb{N}$), and let $\alpha$ be a join-semilattice. For any function $f : \iota \to \alpha$, the sequence of partial suprema $\mathrm{partialSups}(f) : \iota \to \alpha$ is monotone. That is, for any $i, j \in \iota$ with $i \leq j$, we have \[ \mathrm{partialSups}(f)(i) \leq \mathrm{partialSups}(f)(j). \] Here, $\mathrm{partialSups}(f)(i) = \bigsqcup_{k \leq i} f(k)$ denotes the supremum of all $f(k)$ for $k \leq i$.
partialSups.gi definition
: GaloisInsertion (partialSups : (ι → α) → ι →o α) (↑)
Full source 
/-- `partialSups` forms a Galois insertion with the coercion from monotone functions to functions.
-/
def partialSups.gi :
    GaloisInsertion (partialSups : (ι → α) → ι →o α) (↑) where
  choice f h :=
    ⟨f, by convert (partialSups f).monotone using 1; exact (le_partialSups f).antisymm h⟩
  gc f g := by
    refine ⟨(le_partialSups f).trans, fun h ↦ ?_⟩
    convert partialSups_mono h
    exact OrderHom.ext _ _ g.monotone.partialSups_eq.symm
  le_l_u f := le_partialSups f
  choice_eq f h := OrderHom.ext _ _ ((le_partialSups f).antisymm h)
Galois insertion between functions and their partial suprema
Informal description
The construction `partialSups` forms a Galois insertion with the coercion from monotone functions to functions. Specifically, for a preorder $\iota$ where all bounded-above intervals are finite (such as $\mathbb{N}$) and a join-semilattice $\alpha$, the map `partialSups : (ι → α) → ι →o α` (which sends a function to its sequence of partial suprema) and the coercion `↑ : (ι →o α) → (ι → α)` (which forgets the monotonicity) satisfy the properties of a Galois insertion. This means: 1. For any function $f : \iota \to \alpha$, the partial suprema sequence `partialSups f` is monotone. 2. For any monotone function $g : \iota \to_o \alpha$, the partial suprema of its underlying function `g` (viewed as a function) recovers `g` itself, i.e., `partialSups (↑g) = g`. 3. The construction is order-preserving in the sense that if $f_1 \leq f_2$ (pointwise), then `partialSups f_1 ≤ partialSups f_2` (as order homomorphisms).
Pi.partialSups_apply theorem
{τ : Type*} {π : τ → Type*} [∀ t, SemilatticeSup (π t)] (f : ι → (t : τ) → π t) (i : ι) (t : τ) : partialSups f i t = partialSups (f · t) i
Full source 
protected lemma Pi.partialSups_apply {τ : Type*} {π : τ → Type*} [∀ t, SemilatticeSup (π t)]
    (f : ι → (t : τ) → π t) (i : ι) (t : τ) :
    partialSups f i t = partialSups (f · t) i := by
  simp only [partialSups_apply, Finset.sup'_apply]
Componentwise Partial Suprema Equality for Product Types
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite, and let $\tau$ be a type. For each $t \in \tau$, let $\pi_t$ be a join-semilattice. Given a function $f : \iota \to \prod_{t \in \tau} \pi_t$ and an element $i \in \iota$, the value of the partial supremum sequence at $i$ and $t$ equals the partial supremum of the $t$-th component function evaluated at $i$. That is, for any $t \in \tau$, \[ (\text{partialSups}\, f)(i)(t) = \text{partialSups}\, (f(\cdot)(t))(i). \]
partialSups_succ theorem
[LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] (f : ι → α) (i : ι) : partialSups f (Order.succ i) = partialSups f i ⊔ f (Order.succ i)
Full source 
@[simp]
theorem partialSups_succ [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι]
    (f : ι → α) (i : ι) :
    partialSups f (Order.succ i) = partialSupspartialSups f i ⊔ f (Order.succ i) := by
  suffices Iic (Order.succ i) = IicIic i ∪ {Order.succ i} by simp only [partialSups_apply, this,
    sup'_union nonempty_Iic ⟨_, mem_singleton_self _⟩ f, sup'_singleton]
  ext
  simp only [mem_Iic, mem_union, mem_singleton]
  constructor
  · exact fun h ↦ (Order.le_succ_iff_eq_or_le.mp h).symm
  · exact fun h ↦ h.elim (le_trans · <| Order.le_succ _) le_of_eq
Recurrence for Partial Suprema at Successor: $\text{partialSups}(f)(\text{succ}(i)) = \text{partialSups}(f)(i) \sqcup f(\text{succ}(i))$
Informal description
Let $\iota$ be a linearly ordered set where all lower-bounded intervals are finite and equipped with a successor function. For any join-semilattice $\alpha$ and any function $f : \iota \to \alpha$, the partial supremum sequence satisfies the recurrence relation: \[ \text{partialSups}(f)(\text{succ}(i)) = \text{partialSups}(f)(i) \sqcup f(\text{succ}(i)) \] for all $i \in \iota$. Here, $\text{partialSups}(f)(i) = \bigsqcup_{j \leq i} f(j)$ is the supremum of $f$ over all elements less than or equal to $i$.
partialSups_bot theorem
[PartialOrder ι] [LocallyFiniteOrder ι] [OrderBot ι] (f : ι → α) : partialSups f ⊥ = f ⊥
Full source 
@[simp]
theorem partialSups_bot [PartialOrder ι] [LocallyFiniteOrder ι] [OrderBot ι]
    (f : ι → α) : partialSups f ⊥ = f ⊥ := by
  simp only [partialSups_apply]
  -- should we add a lemma `Finset.Iic_bot`?
  suffices Iic (⊥ : ι) = {⊥} by simp only [this, sup'_singleton]
  simp only [← coe_eq_singleton, coe_Iic, Set.Iic_bot]
Partial Supremum at Bottom Element: $\text{partialSups}(f)(\bot) = f(\bot)$
Informal description
Let $\iota$ be a partially ordered set with a bottom element $\bot$ and locally finite order structure, and let $\alpha$ be a join-semilattice. For any function $f \colon \iota \to \alpha$, the partial supremum of $f$ evaluated at $\bot$ equals $f(\bot)$, i.e., \[ \text{partialSups}(f)(\bot) = f(\bot). \]
partialSups_zero theorem
(f : ℕ → α) : partialSups f 0 = f 0
Full source 
@[simp]
theorem partialSups_zero (f : ℕ → α) : partialSups f 0 = f 0 :=
  partialSups_bot f
Partial Supremum at Zero: $\text{partialSups}(f)(0) = f(0)$
Informal description
For any sequence $f \colon \mathbb{N} \to \alpha$ in a join-semilattice $\alpha$, the partial supremum at $0$ equals $f(0)$, i.e., \[ \text{partialSups}(f)(0) = f(0). \]
partialSups_eq_sup'_range theorem
(f : ℕ → α) (n : ℕ) : partialSups f n = (Finset.range (n + 1)).sup' nonempty_range_succ f
Full source 
theorem partialSups_eq_sup'_range (f : ℕ → α) (n : ℕ) :
    partialSups f n = (Finset.range (n + 1)).sup' nonempty_range_succ f :=
  eq_of_forall_ge_iff fun _ ↦ by simp [Nat.lt_succ_iff]
Partial Supremum Equals Finite Range Supremum for Natural Numbers
Informal description
For any sequence $f \colon \mathbb{N} \to \alpha$ in a join-semilattice $\alpha$ and any natural number $n$, the partial supremum $\text{partialSups}(f)(n)$ is equal to the supremum of the values $\{f(k) \mid k \in \{0, \dots, n\}\}$, computed as $\bigsqcup_{k \in \{0, \dots, n\}} f(k)$.
partialSups_eq_sup_range theorem
[OrderBot α] (f : ℕ → α) (n : ℕ) : partialSups f n = (Finset.range (n + 1)).sup f
Full source 
theorem partialSups_eq_sup_range [OrderBot α] (f : ℕ → α) (n : ℕ) :
    partialSups f n = (Finset.range (n + 1)).sup f :=
  eq_of_forall_ge_iff fun _ ↦ by simp [Nat.lt_succ_iff]
Partial Supremum Equals Finite Supremum in Join-Semilattice with Bottom
Informal description
Let $\alpha$ be a join-semilattice with a bottom element $\bot$. For any function $f \colon \mathbb{N} \to \alpha$ and any natural number $n$, the partial supremum $\text{partialSups}(f)(n)$ is equal to the supremum of the set $\{f(k) \mid k \in \{0, \dots, n\}\}$.
disjoint_partialSups_left theorem
{f : ι → α} {i : ι} {x : α} : Disjoint (partialSups f i) x ↔ ∀ j ≤ i, Disjoint (f j) x
Full source 
@[simp]
lemma disjoint_partialSups_left {f : ι → α} {i : ι} {x : α} :
    DisjointDisjoint (partialSups f i) x ↔ ∀ j ≤ i, Disjoint (f j) x :=
  partialSups_iff_forall (Disjoint · x) disjoint_sup_left
Disjointness Characterization for Partial Suprema: Left Version
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite (e.g., $\mathbb{N}$), and let $\alpha$ be a join-semilattice. For any function $f \colon \iota \to \alpha$, any $i \in \iota$, and any $x \in \alpha$, the partial supremum $\bigsqcup_{j \leq i} f(j)$ is disjoint from $x$ if and only if $f(j)$ is disjoint from $x$ for all $j \leq i$. In other words: \[ \text{Disjoint}\left(\bigsqcup_{j \leq i} f(j), x\right) \leftrightarrow \forall j \leq i, \text{Disjoint}(f(j), x). \]
disjoint_partialSups_right theorem
{f : ι → α} {i : ι} {x : α} : Disjoint x (partialSups f i) ↔ ∀ j ≤ i, Disjoint x (f j)
Full source 
@[simp]
lemma disjoint_partialSups_right {f : ι → α} {i : ι} {x : α} :
    DisjointDisjoint x (partialSups f i) ↔ ∀ j ≤ i, Disjoint x (f j) :=
  partialSups_iff_forall (Disjoint x) disjoint_sup_right
Disjointness Characterization for Partial Suprema: Right Version
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite, and let $\alpha$ be a join-semilattice. For any function $f \colon \iota \to \alpha$, any element $x \in \alpha$, and any index $i \in \iota$, the elements $x$ and $\mathrm{partialSups}(f)(i)$ are disjoint if and only if $x$ is disjoint from $f(j)$ for all $j \leq i$. In other words: \[ x \sqcap \left(\bigsqcup_{j \leq i} f(j)\right) = \bot \quad \leftrightarrow \quad \forall j \leq i, x \sqcap f(j) = \bot. \]
partialSups_disjoint_of_disjoint theorem
(f : ι → α) (h : Pairwise (Disjoint on f)) {i j : ι} (hij : i < j) : Disjoint (partialSups f i) (f j)
Full source 
theorem partialSups_disjoint_of_disjoint (f : ι → α) (h : Pairwise (DisjointDisjoint on f))
    {i j : ι} (hij : i < j) :
    Disjoint (partialSups f i) (f j) :=
  disjoint_partialSups_left.2 fun _ hk ↦ h (hk.trans_lt hij).ne
Disjointness of Partial Suprema for Pairwise Disjoint Functions
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite (e.g., $\mathbb{N}$), and let $\alpha$ be a join-semilattice. Given a function $f \colon \iota \to \alpha$ such that $f$ is pairwise disjoint (i.e., $f(i)$ and $f(j)$ are disjoint for all $i \neq j$), then for any $i, j \in \iota$ with $i < j$, the partial supremum $\bigsqcup_{k \leq i} f(k)$ is disjoint from $f(j)$. In other words: \[ \text{Disjoint}\left(\bigsqcup_{k \leq i} f(k), f(j)\right). \]
partialSups_eq_ciSup_Iic theorem
[ConditionallyCompleteLattice α] (f : ι → α) (i : ι) : partialSups f i = ⨆ i : Set.Iic i, f i
Full source 
theorem partialSups_eq_ciSup_Iic [ConditionallyCompleteLattice α] (f : ι → α) (i : ι) :
    partialSups f i = ⨆ i : Set.Iic i, f i := by
  simp only [partialSups_apply]
  apply le_antisymm
  · exact sup'_le _ _ fun j hj ↦ le_ciSup_of_le (Set.finite_range _).bddAbove
      ⟨j, by simpa only [Set.mem_Iic, mem_Iic] using hj⟩ le_rfl
  · exact ciSup_le fun ⟨j, hj⟩ ↦ le_sup' f (by simpa only [mem_Iic, Set.mem_Iic] using hj)
Partial Supremum Equals Indexed Supremum over Lower Interval
Informal description
Let $\alpha$ be a conditionally complete lattice and $\iota$ be a preorder where all lower-closed intervals are finite. For any function $f : \iota \to \alpha$ and any $i \in \iota$, the partial supremum $\text{partialSups}(f)(i)$ (defined as the supremum of $\{f(j) \mid j \leq i\}$) equals the indexed supremum $\bigsqcup_{j \in (-\infty, i]} f(j)$ over the lower-closed interval $(-\infty, i]$.
ciSup_partialSups_eq theorem
[ConditionallyCompleteLattice α] {f : ι → α} (h : BddAbove (Set.range f)) : ⨆ i, partialSups f i = ⨆ i, f i
Full source 
@[simp]
theorem ciSup_partialSups_eq [ConditionallyCompleteLattice α]
    {f : ι → α} (h : BddAbove (Set.range f)) :
    ⨆ i, partialSups f i = ⨆ i, f i := by
  by_cases hι : Nonempty ι
  · refine (ciSup_le fun i ↦ ?_).antisymm (ciSup_mono ?_ <| le_partialSups f)
    · simpa only [partialSups_eq_ciSup_Iic] using ciSup_le fun i ↦ le_ciSup h _
    · rwa [bddAbove_range_partialSups]
  · exact congr_arg _ (funext (not_nonempty_iff.mp hι).elim)
Supremum of Partial Suprema Equals Supremum of Function in Conditionally Complete Lattice
Informal description
Let $\alpha$ be a conditionally complete lattice and $\iota$ be a preorder where all bounded-above intervals are finite. For any function $f \colon \iota \to \alpha$ such that the range of $f$ is bounded above, the supremum of the partial suprema of $f$ equals the supremum of $f$, i.e., \[ \bigsqcup_{i \in \iota} \left( \bigsqcup_{j \leq i} f(j) \right) = \bigsqcup_{i \in \iota} f(i). \]
ciSup_partialSups_eq' theorem
[ConditionallyCompleteLinearOrder α] (f : ι → α) : ⨆ i, partialSups f i = ⨆ i, f i
Full source 
/-- Version of `ciSup_partialSups_eq` without boundedness assumptions, but requiring a
`ConditionallyCompleteLinearOrder` rather than just a `ConditionallyCompleteLattice`. -/
@[simp]
theorem ciSup_partialSups_eq' [ConditionallyCompleteLinearOrder α] (f : ι → α) :
    ⨆ i, partialSups f i = ⨆ i, f i := by
  by_cases h : BddAbove (Set.range f)
  · exact ciSup_partialSups_eq h
  · rw [iSup, iSup, ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ h,
      ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _
        (bddAbove_range_partialSups.not.mpr h)]
Supremum of Partial Suprema Equals Supremum of Function in Conditionally Complete Linear Order
Informal description
Let $\alpha$ be a conditionally complete linear order and $\iota$ be a preorder where all bounded-above intervals are finite. For any function $f \colon \iota \to \alpha$, the supremum of the partial suprema of $f$ equals the supremum of $f$, i.e., \[ \bigsqcup_{i \in \iota} \left( \bigsqcup_{j \leq i} f(j) \right) = \bigsqcup_{i \in \iota} f(i). \]
iSup_partialSups_eq theorem
(f : ι → α) : ⨆ i, partialSups f i = ⨆ i, f i
Full source 
/-- Version of `ciSup_partialSups_eq` without boundedness assumptions, but requiring a
`CompleteLattice` rather than just a `ConditionallyCompleteLattice`. -/
theorem iSup_partialSups_eq (f : ι → α) :
    ⨆ i, partialSups f i = ⨆ i, f i :=
  ciSup_partialSups_eq <| OrderTop.bddAbove _
Supremum of Partial Suprema Equals Supremum of Function in Complete Lattice
Informal description
Let $\alpha$ be a complete lattice and $\iota$ be a preorder where all bounded-above intervals are finite (such as $\mathbb{N}$). For any function $f \colon \iota \to \alpha$, the supremum of the sequence of partial suprema of $f$ equals the supremum of $f$, i.e., \[ \bigsqcup_{i \in \iota} \left( \bigsqcup_{j \leq i} f(j) \right) = \bigsqcup_{i \in \iota} f(i). \]
partialSups_eq_biSup theorem
(f : ι → α) (i : ι) : partialSups f i = ⨆ j ≤ i, f j
Full source 
theorem partialSups_eq_biSup (f : ι → α) (i : ι) :
    partialSups f i = ⨆ j ≤ i, f j := by
  simpa only [iSup_subtype] using partialSups_eq_ciSup_Iic f i
Partial Supremum Equals Indexed Supremum over Lower Set
Informal description
Let $\iota$ be a preorder where all intervals bounded above are finite (e.g., $\mathbb{N}$), and let $\alpha$ be a join-semilattice. For any function $f : \iota \to \alpha$ and any $i \in \iota$, the partial supremum $\mathrm{partialSups}(f)(i)$ (defined as the supremum of $\{f(j) \mid j \leq i\}$) equals the indexed supremum $\bigsqcup_{j \leq i} f(j)$.
iSup_le_iSup_of_partialSups_le_partialSups theorem
{f g : ι → α} (h : partialSups f ≤ partialSups g) : ⨆ i, f i ≤ ⨆ i, g i
Full source 
theorem iSup_le_iSup_of_partialSups_le_partialSups {f g : ι → α}
    (h : partialSups f ≤ partialSups g) : ⨆ i, f i ≤ ⨆ i, g i := by
  rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g]
  exact iSup_mono h
Comparison of Suprema via Partial Suprema
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite (such as $\mathbb{N}$), and let $\alpha$ be a complete lattice. For any two functions $f, g \colon \iota \to \alpha$, if the sequence of partial suprema of $f$ is pointwise less than or equal to that of $g$ (i.e., $\mathrm{partialSups}(f)(i) \leq \mathrm{partialSups}(g)(i)$ for all $i \in \iota$), then the supremum of $f$ is less than or equal to the supremum of $g$, i.e., \[ \bigsqcup_{i \in \iota} f(i) \leq \bigsqcup_{i \in \iota} g(i). \]
iSup_eq_iSup_of_partialSups_eq_partialSups theorem
{f g : ι → α} (h : partialSups f = partialSups g) : ⨆ i, f i = ⨆ i, g i
Full source 
theorem iSup_eq_iSup_of_partialSups_eq_partialSups {f g : ι → α}
    (h : partialSups f = partialSups g) : ⨆ i, f i = ⨆ i, g i := by
  simp_rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g, h]
Suprema Equality from Partial Suprema Equality in Complete Lattices
Informal description
Let $\iota$ be a preorder where all bounded-above intervals are finite (such as $\mathbb{N}$), and let $\alpha$ be a complete lattice. For any two functions $f, g \colon \iota \to \alpha$, if their sequences of partial suprema are equal (i.e., $\mathrm{partialSups}(f) = \mathrm{partialSups}(g)$), then the suprema of $f$ and $g$ are equal: \[ \bigsqcup_{i \in \iota} f(i) = \bigsqcup_{i \in \iota} g(i). \]
partialSups_eq_sUnion_image theorem
[DecidableEq (Set α)] (s : ℕ → Set α) (n : ℕ) : partialSups s n = ⋃₀ ↑((Finset.range (n + 1)).image s)
Full source 
lemma partialSups_eq_sUnion_image [DecidableEq (Set α)] (s : ℕ → Set α) (n : ℕ) :
    partialSups s n = ⋃₀ ↑((Finset.range (n + 1)).image s) := by
  ext; simp [partialSups_eq_biSup, Nat.lt_succ_iff]
Partial Supremum of Sets as Union over Finite Range
Informal description
For a sequence of sets $(s_n)_{n \in \mathbb{N}}$ in a type $\alpha$ with decidable equality, the partial supremum up to index $n$ is equal to the union of the images of the sequence over the finite set $\{0, \dots, n\}$. That is, \[ \mathrm{partialSups}(s)(n) = \bigcup_{k \in \{0, \dots, n\}} s_k. \]
partialSups_eq_biUnion_range theorem
(s : ℕ → Set α) (n : ℕ) : partialSups s n = ⋃ i ∈ Finset.range (n + 1), s i
Full source 
lemma partialSups_eq_biUnion_range (s : ℕ → Set α) (n : ℕ) :
    partialSups s n = ⋃ i ∈ Finset.range (n + 1), s i := by
  ext; simp [partialSups_eq_biSup, Nat.lt_succ]
Partial Supremum of Sets Equals Union over Initial Segment
Informal description
For any sequence of sets $s : \mathbb{N} \to \text{Set } \alpha$ and any natural number $n$, the partial supremum $\text{partialSups}(s)(n)$ (defined as the supremum of $\{s(i) \mid i \leq n\}$) equals the union of the sets $\{s(i) \mid i \in \{0, \dots, n\}\}$. In other words, the partial supremum up to $n$ is the union of the first $n+1$ sets in the sequence: $$\text{partialSups}(s)(n) = \bigcup_{i=0}^n s(i).$$