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

source

noncomputable def real.sign (r : ℝ) :

ℝ

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

Equations

r.sign = ite (r < 0) (-1) (ite (0 < r) 1 0)

source

theorem real.sign_of_neg {r : ℝ} (hr : r < 0) :

r.sign = -1

source

theorem real.sign_of_pos {r : ℝ} (hr : 0 < r) :

r.sign = 1

source

@[simp]

theorem real.sign_zero :

0.sign = 0

source

@[simp]

theorem real.sign_one :

1.sign = 1

source

theorem real.sign_apply_eq (r : ℝ) :

r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

source

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 ℝˣ

source

@[simp]

theorem real.sign_eq_zero_iff {r : ℝ} :

r.sign = 0 ↔ r = 0

source

theorem real.sign_int_cast (z : ℤ) :

↑z.sign = ↑(z.sign)

source

theorem real.sign_neg {r : ℝ} :

(-r).sign = -r.sign

source

theorem real.sign_mul_nonneg (r : ℝ) :

0 ≤ r.sign * r

source

theorem real.sign_mul_pos_of_ne_zero (r : ℝ) (hr : r ≠ 0) :

0 < r.sign * r

source

@[simp]

theorem real.inv_sign (r : ℝ) :

(r.sign)⁻¹ = r.sign

source

@[simp]

theorem real.sign_inv (r : ℝ) :

r⁻¹.sign = r.sign