Set.Ioo_infinite
theorem Set.Ioo_infinite :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DenselyOrdered α] {a b : α}, a < b → (Set.Ioo a b).Infinite := by
sorry
This theorem states that for any type `α` that has a preorder and is densely ordered, and for any two elements `a` and `b` of this type such that `a` is less than `b`, the left-open right-open interval between `a` and `b` (denoted as `(a,b)`) is infinite. In other words, there are infinitely many elements in the type `α` that are strictly greater than `a` and strictly less than `b`.
More concisely: For any densely ordered type `α` with a preorder, the interval `(a, b)` between any `a < b` in `α` is infinite.
|
Set.Icc_infinite
theorem Set.Icc_infinite :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DenselyOrdered α] {a b : α}, a < b → (Set.Icc a b).Infinite := by
sorry
The theorem `Set.Icc_infinite` states that for any type `α` that is equipped with a preorder and is densely ordered, and for any two elements `a` and `b` of `α` where `a` is strictly less than `b`, the left-closed right-closed interval from `a` to `b` (denoted `Set.Icc a b`) is infinite. In other words, there are infinitely many elements in the interval between `a` and `b`.
More concisely: For any densely ordered type `α` with a preorder, every strictly increasing interval `I = {x : α | a ≤ x ≤ b}` is infinite.
|
NoMaxOrder.infinite
theorem NoMaxOrder.infinite :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Nonempty α] [inst : NoMaxOrder α], Infinite α
This theorem states that for any nonempty type `α` that is a preorder and has no maximal element (i.e., there's always an element larger than any given one), then `α` is infinite. This means that we can always find a new, distinct element in `α`, no matter how many elements we've already considered. This theorem is not an instance, to avoid a cyclic dependency with the implications `Infinite α → Nontrivial α → Nonempty α`.
More concisely: If `α` is a nonempty preorder type without a maximal element, then `α` is infinite.
|
NoMinOrder.infinite
theorem NoMinOrder.infinite :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Nonempty α] [inst : NoMinOrder α], Infinite α
This theorem states that for any type `α`, if `α` has a preorder relation (meaning that `α` is a set where we can tell whether any given pair of elements are in a certain order, but not necessarily a unique order), `α` is nonempty (i.e., there exists at least one element in `α`), and `α` has no minimal element (i.e., there is no element in `α` that is less than or equal to every other element), then `α` must be infinite (i.e., `α` has an unlimited number of elements). This theorem is not declared as an instance to avoid cycle with the propositions `Infinite α → Nontrivial α → Nonempty α`.
More concisely: If a non-empty type `α` with a preorder relation has no minimal element, then `α` is infinite.
|