Mathlib.Data.Nat.Cast.SetInterval._auxLemma.1
theorem Mathlib.Data.Nat.Cast.SetInterval._auxLemma.1 :
∀ {α : Type u_1} [inst : Preorder α] {a : α}, (Set.Ici a).OrdConnected = True
The theorem `Mathlib.Data.Nat.Cast.SetInterval._auxLemma.1` states that for any type `α` with a preorder and any element `a` of type `α`, the left-closed right-infinite interval starting from `a` (denoted as `Set.Ici a`) is order-connected. In mathematical terms, it means that for any two points `x` and `y` in the interval `Set.Ici a` where `x ≤ y`, all points `z` such that `x ≤ z ≤ y` are also in `Set.Ici a`.
More concisely: For any type `α` with a preorder and any element `a` of type `α`, the left-closed right-infinite interval `Set.Ici a` is an order-connected set. (That is, all points `x ≤ y` in the interval have all points `z` between them also in the interval.)
|
Nat.range_cast_int
theorem Nat.range_cast_int : Set.range Nat.cast = Set.Ici 0
This theorem states that the range of the natural number casting function to integers is equivalent to the set of all integers that are greater than or equal to 0. In other words, when every natural number is cast to an integer, the resulting set of integers is the same as the set of all integers greater than or equal to 0. This is symbolically represented as: $range(Nat.cast) = [0, \infty)$.
More concisely: The range of the natural number to integer casting function equals the set of integers greater than or equal to zero.
|