Documentation

Mathlib.Data.Real.Sign

Real sign function #

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 #

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
  • r.sign = if r < 0 then -1 else if 0 < r then 1 else 0
Instances For
    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]
    @[simp]
    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_intCast (z : ) :
    (z).sign = z.sign
    @[deprecated Real.sign_intCast]
    theorem Real.sign_int_cast (z : ) :
    (z).sign = z.sign

    Alias of Real.sign_intCast.

    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 : ) :
    r.sign⁻¹ = r.sign
    @[simp]
    theorem Real.sign_inv (r : ) :
    r⁻¹.sign = r.sign