Int.exists_greatest_of_bdd
theorem Int.exists_greatest_of_bdd :
∀ {P : ℤ → Prop}, (∃ b, ∀ (z : ℤ), P z → z ≤ b) → (∃ z, P z) → ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
This theorem states that if we have a predicate `P : ℤ → Prop` such that the set of integers, `{m : P m}`, that satisfy this predicate is bounded above and nonempty, then this set has a greatest element, denoted as `ub`. That is, there exists an integer `ub` such that `P ub` and for any integer `z` that satisfies `P`, `z` is less than or equal to `ub`. This theorem uses classical logic and does not require the predicate `P` to be decidable. There is a constructive counterpart to this theorem, `Int.greatestOfBdd`, which does require decidability of `P`.
More concisely: If `P : ℤ → Prop` is a nonempty, bounded above predicate on integers, then it has a greatest element.
|
Int.exists_least_of_bdd
theorem Int.exists_least_of_bdd :
∀ {P : ℤ → Prop}, (∃ b, ∀ (z : ℤ), P z → b ≤ z) → (∃ z, P z) → ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
The theorem `Int.exists_least_of_bdd` states that if we have a predicate `P` on the set of integers such that the set of integers satisfying `P` is nonempty and bounded below, then there exists a least integer that satisfies `P`. In other words, if there's at least one integer that makes `P` true and there's a lower bound for these integers, then there's a smallest integer that makes `P` true. This theorem uses classical logic, and does not require the predicate `P` to be decidable. For a version of the theorem that works constructively, see `Int.leastOfBdd`.
More concisely: If a nonempty and bounded below subset of integers has a lowest element, then there exists an integer that is the least element of that subset. (Classical logic)
|