Documentation

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Inverse trigonometric functions. #

See also Analysis.SpecialFunctions.Trigonometric.Arctan for the inverse tan function. (This is delayed as it is easier to set up after developing complex trigonometric functions.)

Basic inequalities on trigonometric functions.

noncomputable def Real.arcsin :

Inverse of the sin function, returns values in the range -π / 2 ≤ arcsin x ≤ π / 2. It defaults to -π / 2 on (-∞, -1) and to π / 2 to (1, ∞).

Equations
Instances For
    theorem Real.arcsin_projIcc (x : ) :
    Real.arcsin ↑(Set.projIcc (-1) 1 (_ : -1 1) x) = Real.arcsin x
    theorem Real.sin_arcsin' {x : } (hx : x Set.Icc (-1) 1) :
    theorem Real.sin_arcsin {x : } (hx₁ : -1 x) (hx₂ : x 1) :
    theorem Real.arcsin_sin' {x : } (hx : x Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) :
    theorem Real.arcsin_sin {x : } (hx₁ : -(Real.pi / 2) x) (hx₂ : x Real.pi / 2) :
    theorem Real.arcsin_inj {x : } {y : } (hx₁ : -1 x) (hx₂ : x 1) (hy₁ : -1 y) (hy₂ : y 1) :
    theorem Real.arcsin_eq_of_sin_eq {x : } {y : } (h₁ : Real.sin x = y) (h₂ : x Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) :
    @[simp]
    theorem Real.arcsin_of_one_le {x : } (hx : 1 x) :
    @[simp]
    theorem Real.arcsin_le_iff_le_sin {x : } {y : } (hx : x Set.Icc (-1) 1) (hy : y Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) :
    theorem Real.le_arcsin_iff_sin_le {x : } {y : } (hx : x Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (hy : y Set.Icc (-1) 1) :
    theorem Real.arcsin_lt_iff_lt_sin {x : } {y : } (hx : x Set.Icc (-1) 1) (hy : y Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) :
    theorem Real.arcsin_lt_iff_lt_sin' {x : } {y : } (hy : y Set.Ioc (-(Real.pi / 2)) (Real.pi / 2)) :
    theorem Real.lt_arcsin_iff_sin_lt {x : } {y : } (hx : x Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (hy : y Set.Icc (-1) 1) :
    theorem Real.lt_arcsin_iff_sin_lt' {x : } {y : } (hx : x Set.Ico (-(Real.pi / 2)) (Real.pi / 2)) :
    theorem Real.arcsin_eq_iff_eq_sin {x : } {y : } (hy : y Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) :
    @[simp]
    theorem Real.arcsin_nonneg {x : } :
    @[simp]
    theorem Real.arcsin_nonpos {x : } :
    @[simp]
    theorem Real.arcsin_eq_zero_iff {x : } :
    Real.arcsin x = 0 x = 0
    @[simp]
    theorem Real.zero_eq_arcsin_iff {x : } :
    0 = Real.arcsin x x = 0
    @[simp]
    theorem Real.arcsin_pos {x : } :
    0 < Real.arcsin x 0 < x
    @[simp]
    theorem Real.arcsin_lt_zero {x : } :
    Real.arcsin x < 0 x < 0

    Real.sin as a LocalHomeomorph between (-π / 2, π / 2) and (-1, 1).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable def Real.arccos (x : ) :

      Inverse of the cos function, returns values in the range 0 ≤ arccos x and arccos x ≤ π. It defaults to π on (-∞, -1) and to 0 to (1, ∞).

      Equations
      Instances For
        @[simp]
        theorem Real.arccos_pos {x : } :
        0 < Real.arccos x x < 1
        theorem Real.cos_arccos {x : } (hx₁ : -1 x) (hx₂ : x 1) :
        theorem Real.arccos_cos {x : } (hx₁ : 0 x) (hx₂ : x Real.pi) :
        theorem Real.arccos_inj {x : } {y : } (hx₁ : -1 x) (hx₂ : x 1) (hy₁ : -1 y) (hy₂ : y 1) :
        @[simp]
        @[simp]
        theorem Real.arccos_eq_zero {x : } :
        @[simp]
        theorem Real.arccos_of_one_le {x : } (hx : 1 x) :
        theorem Real.arccos_eq_arcsin {x : } (h : 0 x) :
        theorem Real.arcsin_eq_arccos {x : } (h : 0 x) :