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, ∞).

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).

    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, ∞).

      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) :