data.real.sign

# Real sign function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file introduces and contains some results about real.sign which maps negative real numbers to -1, positive real numbers to 1, and 0 to 0.

## Main definitions #

• real.sign r is $\begin{cases} -1 & \text{if } r < 0, \\ ~~\, 0 & \text{if } r = 0, \\ ~~\, 1 & \text{if } r > 0. \end{cases}$

## Tags #

sign function

noncomputable def real.sign (r : ) :

The sign function that maps negative real numbers to -1, positive numbers to 1, and 0 otherwise.

Equations
theorem real.sign_of_neg {r : } (hr : r < 0) :
r.sign = -1
theorem real.sign_of_pos {r : } (hr : 0 < r) :
r.sign = 1
@[simp]
theorem real.sign_zero  :
0.sign = 0
@[simp]
theorem real.sign_one  :
1.sign = 1
theorem real.sign_apply_eq (r : ) :
r.sign = -1 r.sign = 0 r.sign = 1
theorem real.sign_apply_eq_of_ne_zero (r : ) (h : r 0) :
r.sign = -1 r.sign = 1

This lemma is useful for working with ℝˣ

@[simp]
theorem real.sign_eq_zero_iff {r : } :
r.sign = 0 r = 0
theorem real.sign_int_cast (z : ) :
theorem real.sign_neg {r : } :
(-r).sign = -r.sign
theorem real.sign_mul_nonneg (r : ) :
0 r.sign * r
theorem real.sign_mul_pos_of_ne_zero (r : ) (hr : r 0) :
0 < r.sign * r
@[simp]
theorem real.inv_sign (r : ) :
@[simp]
theorem real.sign_inv (r : ) :