partialSups_succ
theorem partialSups_succ :
∀ {α : Type u_1} [inst : SemilatticeSup α] (f : ℕ → α) (n : ℕ),
(partialSups f) (n + 1) = (partialSups f) n ⊔ f (n + 1)
The theorem `partialSups_succ` states that for any semilattice (a partially ordered set with a supremum for any nonempty finite subset) of type `α` and any function `f` from natural numbers to `α`, the value of the sequence `partialSups f` at `n + 1` is equal to the sup (supremum) of the value of the sequence `partialSups f` at `n` and the value of `f` at `n + 1`. Essentially, this theorem shows how expanding the sequence `partialSups f` by one more term involves taking the supremum of the previous maximum and the next term of `f`.
More concisely: For any semilattice α and function f from natural numbers to α, the sequence of suprema of finite nonempty subsets of the image of f forms a monotonically increasing sequence, and the value at n + 1 is the supremum of the values at n and f(n + 1).
|
le_partialSups_of_le
theorem le_partialSups_of_le :
∀ {α : Type u_1} [inst : SemilatticeSup α] (f : ℕ → α) {m n : ℕ}, m ≤ n → f m ≤ (partialSups f) n
This theorem states that for any type `α` that forms a semilattice with a supremum operation, and for any function `f` from the natural numbers to `α`, if `m` is less than or equal to `n`, then the value of `f` at `m` is less than or equal to the value of the monotone sequence `partialSups f` at `n`. The `partialSups` function generates a sequence whose value at any natural number `n` is the supremum of the values of `f m` for all `m` less than or equal to `n`.
More concisely: For any semilattice `α` with supremum operation and any function `f` from the natural numbers to `α`, if `m ≤ n`, then `f m ≤ sup {f x | x ≤ n}`.
|
Mathlib.Order.PartialSups._auxLemma.3
theorem Mathlib.Order.PartialSups._auxLemma.3 :
∀ {α : Type u_1} [inst : SemilatticeSup α] {f : ℕ → α} {n : ℕ} {a : α},
((partialSups f) n ≤ a) = ∀ k ≤ n, f k ≤ a
The theorem states that for any type `α` that forms a semilattice under a supremum operation, for any function `f` from natural numbers to `α`, for any natural number `n`, and for any element `a` of `α`, the following two conditions are equivalent: (1) the `n`-th element of the sequence of partial supremums of `f` is less than or equal to `a`, and (2) for all natural numbers `k` less than or equal to `n`, the `k`-th element of `f` is less than or equal to `a`. In other words, the maximum value of the function `f` up to the `n`-th term is less than or equal to `a` if and only if all terms of `f` up to the `n`-th term are less than or equal to `a`.
More concisely: For any semilattice `α` with supremum operation, and any function `f` from natural numbers to `α`, the sequence of partial supremums of `f` up to the `n`-th term is less than or equal to an element `a` if and only if the first `n` terms of `f` are less than or equal to `a`.
|
partialSups_le_iff
theorem partialSups_le_iff :
∀ {α : Type u_1} [inst : SemilatticeSup α] {f : ℕ → α} {n : ℕ} {a : α}, (partialSups f) n ≤ a ↔ ∀ k ≤ n, f k ≤ a
The theorem `partialSups_le_iff` states that for any type `α` with a semilattice structure, any function `f` from natural numbers to `α`, any natural number `n`, and any element `a` of `α`, the `n`th partial supremum of `f` is less than or equal to `a` if and only if all the values `f(k)` for `k` less than or equal to `n` are also less than or equal to `a`. This essentially describes a property of the sequence of partial suprema: a bound on the `n`th partial supremum is equivalent to a bound on all the sequence elements up to `n`.
More concisely: For any semilattice type `α`, function `f` from natural numbers to `α`, natural number `n`, and element `a` of `α`, the `n`-th partial supremum of `f` is less than or equal to `a` if and only if all `f(k)` for `k` less than or equal to `n` are less than or equal to `a`.
|
partialSups_iff_forall
theorem partialSups_iff_forall :
∀ {α : Type u_1} [inst : SemilatticeSup α] {f : ℕ → α} (p : α → Prop),
(∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b) → ∀ {n : ℕ}, p ((partialSups f) n) ↔ ∀ k ≤ n, p (f k)
The theorem `partialSups_iff_forall` states that for any type `α` that forms a semilattice with a supremum operation, for any function `f` from natural numbers to `α`, and for any property `p` about elements of `α`, if the property `p` distributes over the supremum operation (meaning that `p` holds for the supremum of `a` and `b` if and only if `p` holds for both `a` and `b`), then the property `p` holds for the `n`-th element of the sequence of partial supremums of `f` if and only if `p` holds for all elements `f k` where `k` is a natural number less than or equal to `n`.
More concisely: For any semilattice `α` with supremum operation, function `f` from natural numbers to `α`, and property `p` distributive over suprema, `p` holds for the `n`-th partial supremum of `f` if and only if `p` holds for all `f k` for `k` up to `n`.
|
le_partialSups
theorem le_partialSups : ∀ {α : Type u_1} [inst : SemilatticeSup α] (f : ℕ → α), f ≤ ⇑(partialSups f)
The theorem `le_partialSups` states that for any type `α` which forms a semilattice with a supremum operation and any sequence `f` of elements of type `α` indexed by natural numbers, the element `f(n)` of the sequence is less than or equal to the `n`-th element of the sequence of partial supremums of `f`. In other words, for each natural number `n`, the `n`-th element of `f` is less than or equal to the supremum of the `f(m)` for `m ≤ n`.
More concisely: For any semilattice `α` with supremum operation and sequence `f` of elements from `α` indexed by natural numbers, `f(n) ≤ sup {f(m) | m ≤ n}` for all natural numbers `n`.
|