Nat.iSup_lt_succ
theorem Nat.iSup_lt_succ :
∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ),
⨆ k, ⨆ (_ : k < n + 1), u k = (⨆ k, ⨆ (_ : k < n), u k) ⊔ u n
For any type `α` that is a complete lattice, and any function `u` from the natural numbers to `α`, the least upper bound of the function `u` applied over all natural numbers `k` less than `n + 1` is equal to the join (i.e., maximum or union) of the least upper bound of `u` applied over all natural numbers less than `n` and `u` applied to `n`.
More concisely: For any complete lattice type `α` and function `u` from natural numbers to `α`, the least upper bound of `u` over numbers less than `n + 1` equals the join of the least upper bound over numbers less than `n` and `u` applied to `n`.
|
Nat.sInf_def
theorem Nat.sInf_def : ∀ {s : Set ℕ} (h : s.Nonempty), sInf s = Nat.find h
This theorem states that for any nonempty set `s` of natural numbers, the infimum of `s` (denoted as `sInf s`) is equal to the smallest natural number in `s` found by the `Nat.find` function, with `h` being the proof of `s` being nonempty. The `Nat.find` function returns the smallest natural number in `s` that satisfies a given property, in this case, the property of being in `s`. This theorem essentially characterizes the infimum of a nonempty set of natural numbers in terms of the `Nat.find` function.
More concisely: For any nonempty set `s` of natural numbers, the infimum of `s` is equal to the output of `Nat.find s h`.
|
Nat.sInf_upward_closed_eq_succ_iff
theorem Nat.sInf_upward_closed_eq_succ_iff :
∀ {s : Set ℕ}, (∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s) → ∀ (k : ℕ), sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s := by
sorry
This theorem, `Nat.sInf_upward_closed_eq_succ_iff`, states that for any set `s` of natural numbers, if `s` is upward closed (meaning that for any two natural numbers `k₁` and `k₂`, if `k₁` is less than or equal to `k₂` and `k₁` is in `s`, then `k₂` is also in `s`), then for any natural number `k`, the least upper bound (infimum) of the set `s` equals `k + 1` if and only if `k + 1` is in `s` and `k` is not in `s`.
This theorem connects the concept of upper bounds and specific elements' membership in a set, specifically with respect to the condition of the set being upward closed. This is useful in understanding the structure and properties of sets of natural numbers.
More concisely: Given an upward closed set of natural numbers `s`, the least upper bound of `s` equals `k + 1` if and only if `k + 1` is in `s` and `k` is not.
|
Nat.sInf_mem
theorem Nat.sInf_mem : ∀ {s : Set ℕ}, s.Nonempty → sInf s ∈ s
The theorem `Nat.sInf_mem` states that for any non-empty set `s` of natural numbers, the infimum (greatest lower bound) of the set `s`, denoted as `sInf s`, is an element of the set `s`. This theorem implies that a non-empty set of natural numbers always contains its infimum.
More concisely: Given a non-empty set of natural numbers `s`, its infimum `sInf s` is an element of `s`.
|
Nat.sInf_eq_zero
theorem Nat.sInf_eq_zero : ∀ {s : Set ℕ}, sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
The theorem `Nat.sInf_eq_zero` states that for any set `s` of natural numbers, the infimum of `s` is zero if and only if either zero is an element of `s` or `s` is an empty set. The 'infimum' of a set is the greatest number that is less than or equal to all numbers in the set. For natural numbers, this would be the smallest number in the set. So, this theorem is stating that the smallest number in a set of natural numbers is `0` if and only if `0` is in the set or the set has no elements.
More concisely: The infimum of a set of natural numbers is zero if and only if the set contains the natural number zero or is empty.
|
Nat.sSup_def
theorem Nat.sSup_def : ∀ {s : Set ℕ} (h : ∃ n, ∀ a ∈ s, a ≤ n), sSup s = Nat.find h
This theorem states that for any set `s` of natural numbers, if there exists a natural number `n` such that every element `a` in `s` is less than or equal to `n`, then the supremum (`sSup`) of the set `s` is equal to the smallest natural number satisfying the aforementioned condition. This smallest natural number is found by the function `Nat.find`. Therefore, this theorem connects the notion of a supremum of a set in the natural numbers to the concept of finding the smallest natural number that serves as an upper bound for the set.
More concisely: For any set `s` of natural numbers, if there exists a natural number `n` such that every element `a` in `s` is less than or equal to `n`, then `sSup = n`, where `sSup` is the supremum of `s`.
|
Nat.sInf_empty
theorem Nat.sInf_empty : sInf ∅ = 0
This theorem states that the infimum (greatest lower bound) of an empty set of natural numbers is 0. In other words, because 0 is the smallest natural number, it serves as the infimum for an empty set.
More concisely: The empty set of natural numbers has 0 as its infimum.
|
Nat.iSup_lt_succ'
theorem Nat.iSup_lt_succ' :
∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ),
⨆ k, ⨆ (_ : k < n + 1), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k < n), u (k + 1)
This theorem states that for any type α that forms a complete lattice and a function `u` from natural numbers to α, the supremum (or greatest lower bound) of `u k` for all `k` less than `n + 1` is equal to the supremum of `u 0` and the supremum of `u (k + 1)` for all `k` less than `n`. In mathematical terms, it asserts that `sup_{k < n + 1} u(k) = u(0) ∨ sup_{k < n} u(k + 1)`.
More concisely: For any function `u` from natural numbers to a complete lattice `α`, the supremum of `{u(k) | k < n+1}` equals the supremum of `{u(0)} ∪ {u(k+1) | k < n}`.
|
Nat.sInf_le
theorem Nat.sInf_le : ∀ {s : Set ℕ} {m : ℕ}, m ∈ s → sInf s ≤ m
This theorem states that for any set of natural numbers `s` and any natural number `m`, if `m` is an element of the set `s`, then the infimum (greatest lower bound) of the set `s` is less than or equal to `m`. The function `sInf s` returns the infimum of the set `s`. This implies that `m` is greater than or equal to the smallest natural number in the set `s`, which is the definition of the infimum in the context of natural numbers.
More concisely: For any set of natural numbers `s` and natural number `m`, if `m` is an element of `s`, then the infimum of `s` is less than or equal to `m`. (In other words, `inf s <= m` whenever `m` is in `s`.)
|
Nat.nonempty_of_pos_sInf
theorem Nat.nonempty_of_pos_sInf : ∀ {s : Set ℕ}, 0 < sInf s → s.Nonempty
This theorem, `Nat.nonempty_of_pos_sInf`, states that for all sets `s` of natural numbers, if the infimum of `s` (denoted as `sInf s`) is greater than 0, then the set `s` is not empty. The term "infimum" of a set refers to the greatest number that is less than or equal to all numbers in the set. This theorem is used to affirm that a set of natural numbers `s` is non-empty given that the lower bound or infimum of `s` is greater than 0.
More concisely: If the infimum of a set of natural numbers is positive, then the set is non-empty.
|
Nat.iInf_const_zero
theorem Nat.iInf_const_zero : ∀ {ι : Sort u_1}, ⨅ i, 0 = 0
This theorem states that for any type `ι`, the infimum (greatest lower bound) of the constant function that always returns `0` is `0`. In mathematical terms, for any index set `ι`, the infimum over `ι` of the function that always yields `0` is indeed `0`.
More concisely: For any index set `ι`, the constant function mapping every element to `0` has `0` as its infimum.
|
Mathlib.Data.Nat.Lattice._auxLemma.9
theorem Mathlib.Data.Nat.Lattice._auxLemma.9 : ∀ {s : Set ℕ}, (sInf s = 0) = (0 ∈ s ∨ s = ∅)
This theorem, from the Mathlib library, states that for any set `s` of natural numbers (`ℕ`), the `infimum` (greatest lower bound) of the set being `0` is equivalent to either the number `0` being an element of the set, or the set being the empty set (`∅`). In other words, the smallest element in the set is `0` if and only if `0` is in the set or the set has no elements.
More concisely: The set of natural numbers `s` has an infimum equal to `0` if and only if `0` is an element of `s` or `s` is the empty set.
|