Real.sign_of_neg
theorem Real.sign_of_neg : ∀ {r : ℝ}, r < 0 → r.sign = -1
The theorem `Real.sign_of_neg` states that for all real numbers `r`, if `r` is less than zero, then the sign function of `r` is -1. In other words, this theorem shows that the sign function defined on the set of real numbers correctly assigns -1 to every negative real number.
More concisely: For all real numbers `r`, if `r` is negative then `Real.sign r = -1`.
|
Real.sign_zero
theorem Real.sign_zero : Real.sign 0 = 0
The theorem `Real.sign_zero` states that the sign function applied to the real number 0 is 0. In other words, according to our definition of the sign function for real numbers, where negative numbers are mapped to -1, positive numbers to 1, and 0 is left as is, when we apply this function on 0, we get 0 in return.
More concisely: The sign of real number 0 is 0.
|
Real.sign_apply_eq_of_ne_zero
theorem Real.sign_apply_eq_of_ne_zero : ∀ (r : ℝ), r ≠ 0 → r.sign = -1 ∨ r.sign = 1
This theorem states that for any real number `r` that is not zero, the sign of `r` is either -1 or 1. This is particularly useful when working with the multiplicative group of non-zero real numbers, denoted as `ℝˣ`.
More concisely: For any non-zero real number `r`, the sign of `r` is either -1 or 1.
|
Real.sign_of_pos
theorem Real.sign_of_pos : ∀ {r : ℝ}, 0 < r → r.sign = 1
This theorem states that for any real number `r`, if `r` is greater than 0, then the sign of `r` (as determined by the `Real.sign` function) is 1. In other words, the sign function returns 1 for all positive real numbers.
More concisely: For all real numbers `r` greater than 0, `Real.sign r = 1`.
|