Loogle!
Result
Found 267 definitions mentioning Real.sin. Of these, only the first 200 are shown.
- Real.sin π Mathlib.Data.Complex.Exponential
(x : β) : β - Complex.ofReal_sin π Mathlib.Data.Complex.Exponential
(x : β) : β(Real.sin x) = Complex.sin βx - Complex.sin_ofReal_re π Mathlib.Data.Complex.Exponential
(x : β) : (Complex.sin βx).re = Real.sin x - Real.sin.eq_1 π Mathlib.Data.Complex.Exponential
(x : β) : Real.sin x = (Complex.sin βx).re - Real.sin_le_one π Mathlib.Data.Complex.Exponential
(x : β) : Real.sin x β€ 1 - Real.sin_neg π Mathlib.Data.Complex.Exponential
(x : β) : Real.sin (-x) = -Real.sin x - Real.neg_one_le_sin π Mathlib.Data.Complex.Exponential
(x : β) : -1 β€ Real.sin x - Real.sin_zero π Mathlib.Data.Complex.Exponential
: Real.sin 0 = 0 - Real.abs_sin_le_one π Mathlib.Data.Complex.Exponential
(x : β) : |Real.sin x| β€ 1 - Complex.exp_ofReal_mul_I_im π Mathlib.Data.Complex.Exponential
(x : β) : (Complex.exp (βx * Complex.I)).im = Real.sin x - Real.cot_eq_cos_div_sin π Mathlib.Data.Complex.Exponential
(x : β) : x.cot = Real.cos x / Real.sin x - Real.tan_eq_sin_div_cos π Mathlib.Data.Complex.Exponential
(x : β) : Real.tan x = Real.sin x / Real.cos x - Complex.exp_im π Mathlib.Data.Complex.Exponential
(x : β) : (Complex.exp x).im = Real.exp x.re * Real.sin x.im - Real.tan_mul_cos π Mathlib.Data.Complex.Exponential
{x : β} (hx : Real.cos x β 0) : Real.tan x * Real.cos x = Real.sin x - Real.sin_sq_le_one π Mathlib.Data.Complex.Exponential
(x : β) : Real.sin x ^ 2 β€ 1 - Real.sin_pos_of_pos_of_le_one π Mathlib.Data.Complex.Exponential
{x : β} (hx0 : 0 < x) (hx : x β€ 1) : 0 < Real.sin x - Real.sin_pos_of_pos_of_le_two π Mathlib.Data.Complex.Exponential
{x : β} (hx0 : 0 < x) (hx : x β€ 2) : 0 < Real.sin x - Real.abs_cos_eq_sqrt_one_sub_sin_sq π Mathlib.Data.Complex.Exponential
(x : β) : |Real.cos x| = β(1 - Real.sin x ^ 2) - Real.abs_sin_eq_sqrt_one_sub_cos_sq π Mathlib.Data.Complex.Exponential
(x : β) : |Real.sin x| = β(1 - Real.cos x ^ 2) - Real.cos_add π Mathlib.Data.Complex.Exponential
(x y : β) : Real.cos (x + y) = Real.cos x * Real.cos y - Real.sin x * Real.sin y - Real.cos_sub π Mathlib.Data.Complex.Exponential
(x y : β) : Real.cos (x - y) = Real.cos x * Real.cos y + Real.sin x * Real.sin y - Real.sin_add π Mathlib.Data.Complex.Exponential
(x y : β) : Real.sin (x + y) = Real.sin x * Real.cos y + Real.cos x * Real.sin y - Real.sin_sub π Mathlib.Data.Complex.Exponential
(x y : β) : Real.sin (x - y) = Real.sin x * Real.cos y - Real.cos x * Real.sin y - Real.cos_sq' π Mathlib.Data.Complex.Exponential
(x : β) : Real.cos x ^ 2 = 1 - Real.sin x ^ 2 - Real.cos_sq_add_sin_sq π Mathlib.Data.Complex.Exponential
(x : β) : Real.cos x ^ 2 + Real.sin x ^ 2 = 1 - Real.sin_sq π Mathlib.Data.Complex.Exponential
(x : β) : Real.sin x ^ 2 = 1 - Real.cos x ^ 2 - Real.sin_sq_add_cos_sq π Mathlib.Data.Complex.Exponential
(x : β) : Real.sin x ^ 2 + Real.cos x ^ 2 = 1 - Real.sin_two_mul π Mathlib.Data.Complex.Exponential
(x : β) : Real.sin (2 * x) = 2 * Real.sin x * Real.cos x - Real.tan_div_sqrt_one_add_tan_sq π Mathlib.Data.Complex.Exponential
{x : β} (hx : 0 < Real.cos x) : Real.tan x / β(1 + Real.tan x ^ 2) = Real.sin x - Real.two_mul_sin_mul_cos π Mathlib.Data.Complex.Exponential
(x y : β) : 2 * Real.sin x * Real.cos y = Real.sin (x - y) + Real.sin (x + y) - Real.two_mul_sin_mul_sin π Mathlib.Data.Complex.Exponential
(x y : β) : 2 * Real.sin x * Real.sin y = Real.cos (x - y) - Real.cos (x + y) - Real.cos_two_mul' π Mathlib.Data.Complex.Exponential
(x : β) : Real.cos (2 * x) = Real.cos x ^ 2 - Real.sin x ^ 2 - Real.tan_sq_div_one_add_tan_sq π Mathlib.Data.Complex.Exponential
{x : β} (hx : Real.cos x β 0) : Real.tan x ^ 2 / (1 + Real.tan x ^ 2) = Real.sin x ^ 2 - Real.sin_three_mul π Mathlib.Data.Complex.Exponential
(x : β) : Real.sin (3 * x) = 3 * Real.sin x - 4 * Real.sin x ^ 3 - Real.sin_sq_eq_half_sub π Mathlib.Data.Complex.Exponential
(x : β) : Real.sin x ^ 2 = 1 / 2 - Real.cos (2 * x) / 2 - Real.sin_sub_sin π Mathlib.Data.Complex.Exponential
(x y : β) : Real.sin x - Real.sin y = 2 * Real.sin ((x - y) / 2) * Real.cos ((x + y) / 2) - Real.cos_sub_cos π Mathlib.Data.Complex.Exponential
(x y : β) : Real.cos x - Real.cos y = -2 * Real.sin ((x + y) / 2) * Real.sin ((x - y) / 2) - Real.sin_bound π Mathlib.Data.Complex.Exponential
{x : β} (hx : |x| β€ 1) : |Real.sin x - (x - x ^ 3 / 6)| β€ |x| ^ 4 * (5 / 96) - Real.range_sin_infinite π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: (Set.range Real.sin).Infinite - Real.sin_antiperiodic π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Function.Antiperiodic Real.sin Real.pi - Real.sin_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.sin Real.pi = 0 - Real.continuous_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Continuous Real.sin - Real.sin_pi_sub π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) : Real.sin (Real.pi - x) = Real.sin x - Real.continuousOn_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{s : Set β} : ContinuousOn Real.sin s - Real.sin_add_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) : Real.sin (x + Real.pi) = -Real.sin x - Real.sin_sub_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) : Real.sin (x - Real.pi) = -Real.sin x - Real.sin_int_mul_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(n : β€) : Real.sin (βn * Real.pi) = 0 - Real.sin_nat_mul_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(n : β) : Real.sin (βn * Real.pi) = 0 - Real.mapsTo_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(s : Set β) : Set.MapsTo Real.sin s (Set.Icc (-1) 1) - Real.range_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Set.range Real.sin = Set.Icc (-1) 1 - Real.sin_periodic π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Function.Periodic Real.sin (2 * Real.pi) - Real.sin_mem_Icc π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) : Real.sin x β Set.Icc (-1) 1 - Real.sin_nonneg_of_nonneg_of_le_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x : β} (h0x : 0 β€ x) (hxp : x β€ Real.pi) : 0 β€ Real.sin x - Real.sin_pos_of_pos_of_lt_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x : β} (h0x : 0 < x) (hxp : x < Real.pi) : 0 < Real.sin x - Real.sin_ne_zero_iff π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x : β} : Real.sin x β 0 β β (n : β€), βn * Real.pi β x - Real.sin_nonneg_of_mem_Icc π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x : β} (hx : x β Set.Icc 0 Real.pi) : 0 β€ Real.sin x - Real.sin_pos_of_mem_Ioo π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x : β} (hx : x β Set.Ioo 0 Real.pi) : 0 < Real.sin x - Real.sin_eq_zero_iff π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x : β} : Real.sin x = 0 β β n, βn * Real.pi = x - Real.sin_neg_of_neg_of_neg_pi_lt π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x : β} (hx0 : x < 0) (hpx : -Real.pi < x) : Real.sin x < 0 - Real.sin_nonpos_of_nonnpos_of_neg_pi_le π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x : β} (hx0 : x β€ 0) (hpx : -Real.pi β€ x) : Real.sin x β€ 0 - Real.sin_two_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.sin (2 * Real.pi) = 0 - Real.sin_pi_div_two π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.sin (Real.pi / 2) = 1 - Real.sin_eq_zero_iff_of_lt_of_lt π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x : β} (hxβ : -Real.pi < x) (hxβ : x < Real.pi) : Real.sin x = 0 β x = 0 - Real.sin_add_two_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) : Real.sin (x + 2 * Real.pi) = Real.sin x - Real.sin_sub_two_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) : Real.sin (x - 2 * Real.pi) = Real.sin x - Real.sin_eq_zero_iff_cos_eq π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x : β} : Real.sin x = 0 β Real.cos x = 1 β¨ Real.cos x = -1 - Real.cos_pi_div_two_sub π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) : Real.cos (Real.pi / 2 - x) = Real.sin x - Real.cos_sub_pi_div_two π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) : Real.cos (x - Real.pi / 2) = Real.sin x - Real.sin_add_pi_div_two π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) : Real.sin (x + Real.pi / 2) = Real.cos x - Real.sin_pi_div_two_sub π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) : Real.sin (Real.pi / 2 - x) = Real.cos x - Real.sin_two_pi_sub π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) : Real.sin (2 * Real.pi - x) = -Real.sin x - Real.cos_add_pi_div_two π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) : Real.cos (x + Real.pi / 2) = -Real.sin x - Real.sin_sub_pi_div_two π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) : Real.sin (x - Real.pi / 2) = -Real.cos x - Real.sin_add_int_mul_two_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) (n : β€) : Real.sin (x + βn * (2 * Real.pi)) = Real.sin x - Real.sin_add_nat_mul_two_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) (n : β) : Real.sin (x + βn * (2 * Real.pi)) = Real.sin x - Real.sin_sub_int_mul_two_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) (n : β€) : Real.sin (x - βn * (2 * Real.pi)) = Real.sin x - Real.sin_sub_nat_mul_two_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) (n : β) : Real.sin (x - βn * (2 * Real.pi)) = Real.sin x - Real.sin_int_mul_two_pi_sub π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) (n : β€) : Real.sin (βn * (2 * Real.pi) - x) = -Real.sin x - Real.sin_nat_mul_two_pi_sub π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) (n : β) : Real.sin (βn * (2 * Real.pi) - x) = -Real.sin x - Real.sin_eq_sqrt_one_sub_cos_sq π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x : β} (hl : 0 β€ x) (hu : x β€ Real.pi) : Real.sin x = β(1 - Real.cos x ^ 2) - Real.sin_add_int_mul_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) (n : β€) : Real.sin (x + βn * Real.pi) = (-1) ^ n * Real.sin x - Real.sin_add_nat_mul_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) (n : β) : Real.sin (x + βn * Real.pi) = (-1) ^ n * Real.sin x - Real.sin_pi_div_six π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.sin (Real.pi / 6) = 1 / 2 - Real.sin_sub_int_mul_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) (n : β€) : Real.sin (x - βn * Real.pi) = (-1) ^ n * Real.sin x - Real.sin_sub_nat_mul_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) (n : β) : Real.sin (x - βn * Real.pi) = (-1) ^ n * Real.sin x - Real.injOn_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Set.InjOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) - Real.sin_int_mul_pi_sub π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) (n : β€) : Real.sin (βn * Real.pi - x) = -((-1) ^ n * Real.sin x) - Real.sin_nat_mul_pi_sub π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) (n : β) : Real.sin (βn * Real.pi - x) = -((-1) ^ n * Real.sin x) - Real.strictMonoOn_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: StrictMonoOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) - Real.sin_pi_div_four π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.sin (Real.pi / 4) = β2 / 2 - Real.sin_pi_div_three π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.sin (Real.pi / 3) = β3 / 2 - Real.abs_sin_half π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) : |Real.sin (x / 2)| = β((1 - Real.cos x) / 2) - Real.sin_le_sin_of_le_of_le_pi_div_two π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x y : β} (hxβ : -(Real.pi / 2) β€ x) (hyβ : y β€ Real.pi / 2) (hxy : x β€ y) : Real.sin x β€ Real.sin y - Real.sin_lt_sin_of_lt_of_le_pi_div_two π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x y : β} (hxβ : -(Real.pi / 2) β€ x) (hyβ : y β€ Real.pi / 2) (hxy : x < y) : Real.sin x < Real.sin y - Real.tendsto_sin_pi_div_two π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Filter.Tendsto Real.sin (nhdsWithin (Real.pi / 2) (Set.Iio (Real.pi / 2))) (nhds 1) - Real.bijOn_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Set.BijOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (Set.Icc (-1) 1) - Real.surjOn_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Set.SurjOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (Set.Icc (-1) 1) - Real.sq_sin_pi_div_three π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.sin (Real.pi / 3) ^ 2 = 3 / 4 - Real.tendsto_sin_neg_pi_div_two π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Filter.Tendsto Real.sin (nhdsWithin (-(Real.pi / 2)) (Set.Ioi (-(Real.pi / 2)))) (nhds (-1)) - Real.sin_pi_div_eight π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.sin (Real.pi / 8) = β(2 - β2) / 2 - Real.cos_eq_sqrt_one_sub_sin_sq π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x : β} (hl : -(Real.pi / 2) β€ x) (hu : x β€ Real.pi / 2) : Real.cos x = β(1 - Real.sin x ^ 2) - Real.sin_half_eq_sqrt π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x : β} (hl : 0 β€ x) (hr : x β€ 2 * Real.pi) : Real.sin (x / 2) = β((1 - Real.cos x) / 2) - Real.sin_pi_over_two_pow_succ π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(n : β) : Real.sin (Real.pi / 2 ^ (n + 2)) = β(2 - Real.sqrtTwoAddSeries 0 n) / 2 - Real.sin_pi_div_sixteen π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.sin (Real.pi / 16) = β(2 - β(2 + β2)) / 2 - Real.sin_half_eq_neg_sqrt π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x : β} (hl : -(2 * Real.pi) β€ x) (hr : x β€ 0) : Real.sin (x / 2) = -β((1 - Real.cos x) / 2) - Real.sin_sq_pi_over_two_pow π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(n : β) : Real.sin (Real.pi / 2 ^ (n + 1)) ^ 2 = 1 - (Real.sqrtTwoAddSeries 0 n / 2) ^ 2 - Real.sin_pi_div_thirty_two π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.sin (Real.pi / 32) = β(2 - β(2 + β(2 + β2))) / 2 - Real.sin_sq_pi_over_two_pow_succ π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(n : β) : Real.sin (Real.pi / 2 ^ (n + 2)) ^ 2 = 1 / 2 - Real.sqrtTwoAddSeries 0 n / 4 - Real.coe_sinOrderIso_apply π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β(Set.Icc (-(Real.pi / 2)) (Real.pi / 2))) : β(Real.sinOrderIso x) = Real.sin βx - Real.sinOrderIso_apply π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β(Set.Icc (-(Real.pi / 2)) (Real.pi / 2))) : Real.sinOrderIso x = β¨Real.sin βx, β―β© - Real.Angle.sin_coe π Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
(x : β) : (βx).sin = Real.sin x - Real.Angle.sin_toReal π Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
(ΞΈ : Real.Angle) : Real.sin ΞΈ.toReal = ΞΈ.sin - Real.Angle.cos_sin_inj π Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
{ΞΈ Ο : β} (Hcos : Real.cos ΞΈ = Real.cos Ο) (Hsin : Real.sin ΞΈ = Real.sin Ο) : βΞΈ = βΟ - Real.Angle.sin_eq_real_sin_iff_eq_or_add_eq_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
{ΞΈ : Real.Angle} {Ο : β} : ΞΈ.sin = Real.sin Ο β ΞΈ = βΟ β¨ ΞΈ + βΟ = βReal.pi - Real.Angle.sin_eq_iff_coe_eq_or_add_eq_pi π Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
{ΞΈ Ο : β} : Real.sin ΞΈ = Real.sin Ο β βΞΈ = βΟ β¨ βΞΈ + βΟ = βReal.pi - Real.sin_arcsin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x : β} (hxβ : -1 β€ x) (hxβ : x β€ 1) : Real.sin (Real.arcsin x) = x - Real.sin_arcsin' π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x : β} (hx : x β Set.Icc (-1) 1) : Real.sin (Real.arcsin x) = x - Real.sin_arccos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
(x : β) : Real.sin (Real.arccos x) = β(1 - x ^ 2) - Real.arcsin_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x : β} (hxβ : -(Real.pi / 2) β€ x) (hxβ : x β€ Real.pi / 2) : Real.arcsin (Real.sin x) = x - Real.arcsin_sin' π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x : β} (hx : x β Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) : Real.arcsin (Real.sin x) = x - Real.arcsin_eq_of_sin_eq π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x y : β} (hβ : Real.sin x = y) (hβ : x β Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) : Real.arcsin y = x - Real.arcsin_eq_iff_eq_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x y : β} (hy : y β Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) : Real.arcsin x = y β x = Real.sin y - Real.arcsin_le_iff_le_sin' π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x y : β} (hy : y β Set.Ico (-(Real.pi / 2)) (Real.pi / 2)) : Real.arcsin x β€ y β x β€ Real.sin y - Real.arcsin_lt_iff_lt_sin' π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x y : β} (hy : y β Set.Ioc (-(Real.pi / 2)) (Real.pi / 2)) : Real.arcsin x < y β x < Real.sin y - Real.le_arcsin_iff_sin_le' π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x y : β} (hx : x β Set.Ioc (-(Real.pi / 2)) (Real.pi / 2)) : x β€ Real.arcsin y β Real.sin x β€ y - Real.lt_arcsin_iff_sin_lt' π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x y : β} (hx : x β Set.Ico (-(Real.pi / 2)) (Real.pi / 2)) : x < Real.arcsin y β Real.sin x < y - Real.mapsTo_sin_Ioo π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
: Set.MapsTo Real.sin (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) (Set.Ioo (-1) 1) - Real.arcsin_le_iff_le_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x y : β} (hx : x β Set.Icc (-1) 1) (hy : y β Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) : Real.arcsin x β€ y β x β€ Real.sin y - Real.arcsin_lt_iff_lt_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x y : β} (hx : x β Set.Icc (-1) 1) (hy : y β Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) : Real.arcsin x < y β x < Real.sin y - Real.le_arcsin_iff_sin_le π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x y : β} (hx : x β Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (hy : y β Set.Icc (-1) 1) : x β€ Real.arcsin y β Real.sin x β€ y - Real.lt_arcsin_iff_sin_lt π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x y : β} (hx : x β Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (hy : y β Set.Icc (-1) 1) : x < Real.arcsin y β Real.sin x < y - Real.sinPartialHomeomorph.eq_1 π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
: Real.sinPartialHomeomorph = { toFun := Real.sin, invFun := Real.arcsin, source := Set.Ioo (-(Real.pi / 2)) (Real.pi / 2), target := Set.Ioo (-1) 1, map_source' := Real.mapsTo_sin_Ioo, map_target' := Real.sinPartialHomeomorph.proof_2, left_inv' := Real.sinPartialHomeomorph.proof_3, right_inv' := Real.sinPartialHomeomorph.proof_4, open_source := Real.sinPartialHomeomorph.proof_5, open_target := Real.sinPartialHomeomorph.proof_6, continuousOn_toFun := Real.sinPartialHomeomorph.proof_7, continuousOn_invFun := Real.sinPartialHomeomorph.proof_8 } - Complex.abs_mul_sin_arg π Mathlib.Analysis.SpecialFunctions.Complex.Arg
(x : β) : Complex.abs x * Real.sin x.arg = x.im - Complex.sin_arg π Mathlib.Analysis.SpecialFunctions.Complex.Arg
(x : β) : Real.sin x.arg = x.im / Complex.abs x - Complex.cpow_ofReal_im π Mathlib.Analysis.SpecialFunctions.Pow.Real
(x : β) (y : β) : (x ^ βy).im = Complex.abs x ^ y * Real.sin (x.arg * y) - Complex.cpow_ofReal π Mathlib.Analysis.SpecialFunctions.Pow.Real
(x : β) (y : β) : x ^ βy = β(Complex.abs x ^ y) * (β(Real.cos (x.arg * y)) + β(Real.sin (x.arg * y)) * Complex.I) - Real.measurable_sin π Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
: Measurable Real.sin - Measurable.sin π Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
{Ξ± : Type u_1} {m : MeasurableSpace Ξ±} {f : Ξ± β β} (hf : Measurable f) : Measurable fun x => Real.sin (f x) - Real.logDeriv_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
: logDeriv Real.sin = Real.cot - Real.deriv_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
: deriv Real.sin = Real.cos - Real.hasDerivAt_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
(x : β) : HasDerivAt Real.sin (Real.cos x) x - Real.hasStrictDerivAt_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
(x : β) : HasStrictDerivAt Real.sin (Real.cos x) x - Real.hasDerivAt_cos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
(x : β) : HasDerivAt Real.cos (-Real.sin x) x - Real.hasStrictDerivAt_cos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
(x : β) : HasStrictDerivAt Real.cos (-Real.sin x) x - Real.deriv_cos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{x : β} : deriv Real.cos x = -Real.sin x - Real.deriv_cos' π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
: deriv Real.cos = fun x => -Real.sin x - Real.differentiable_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
: Differentiable β Real.sin - Real.contDiff_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{n : ββ} : ContDiff β n Real.sin - Real.differentiableAt_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{x : β} : DifferentiableAt β Real.sin x - Differentiable.sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} (hc : Differentiable β f) : Differentiable β fun x => Real.sin (f x) - HasDerivAt.sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{f : β β β} {f' x : β} (hf : HasDerivAt f f' x) : HasDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) * f') x - HasStrictDerivAt.sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{f : β β β} {f' x : β} (hf : HasStrictDerivAt f f' x) : HasStrictDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) * f') x - ContDiff.sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {n : ββ} (h : ContDiff β n f) : ContDiff β n fun x => Real.sin (f x) - DifferentiableAt.sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {x : E} (hc : DifferentiableAt β f x) : DifferentiableAt β (fun x => Real.sin (f x)) x - HasDerivAt.cos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{f : β β β} {f' x : β} (hf : HasDerivAt f f' x) : HasDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) * f') x - HasStrictDerivAt.cos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{f : β β β} {f' x : β} (hf : HasStrictDerivAt f f' x) : HasStrictDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) * f') x - DifferentiableOn.sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {s : Set E} (hc : DifferentiableOn β f s) : DifferentiableOn β (fun x => Real.sin (f x)) s - HasDerivWithinAt.sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{f : β β β} {f' x : β} {s : Set β} (hf : HasDerivWithinAt f f' s x) : HasDerivWithinAt (fun x => Real.sin (f x)) (Real.cos (f x) * f') s x - ContDiffAt.sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {x : E} {n : ββ} (hf : ContDiffAt β n f x) : ContDiffAt β n (fun x => Real.sin (f x)) x - ContDiffOn.sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {s : Set E} {n : ββ} (hf : ContDiffOn β n f s) : ContDiffOn β n (fun x => Real.sin (f x)) s - DifferentiableWithinAt.sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {x : E} {s : Set E} (hf : DifferentiableWithinAt β f s x) : DifferentiableWithinAt β (fun x => Real.sin (f x)) s x - HasDerivWithinAt.cos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{f : β β β} {f' x : β} {s : Set β} (hf : HasDerivWithinAt f f' s x) : HasDerivWithinAt (fun x => Real.cos (f x)) (-Real.sin (f x) * f') s x - ContDiffWithinAt.sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {x : E} {s : Set E} {n : ββ} (hf : ContDiffWithinAt β n f s x) : ContDiffWithinAt β n (fun x => Real.sin (f x)) s x - deriv_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{f : β β β} {x : β} (hc : DifferentiableAt β f x) : deriv (fun x => Real.sin (f x)) x = Real.cos (f x) * deriv f x - deriv_cos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{f : β β β} {x : β} (hc : DifferentiableAt β f x) : deriv (fun x => Real.cos (f x)) x = -Real.sin (f x) * deriv f x - derivWithin_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{f : β β β} {x : β} {s : Set β} (hf : DifferentiableWithinAt β f s x) (hxs : UniqueDiffWithinAt β s x) : derivWithin (fun x => Real.sin (f x)) s x = Real.cos (f x) * derivWithin f s x - derivWithin_cos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{f : β β β} {x : β} {s : Set β} (hf : DifferentiableWithinAt β f s x) (hxs : UniqueDiffWithinAt β s x) : derivWithin (fun x => Real.cos (f x)) s x = -Real.sin (f x) * derivWithin f s x - HasFDerivAt.sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {f' : E βL[β] β} {x : E} (hf : HasFDerivAt f f' x) : HasFDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) β’ f') x - HasStrictFDerivAt.sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {f' : E βL[β] β} {x : E} (hf : HasStrictFDerivAt f f' x) : HasStrictFDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) β’ f') x - HasFDerivAt.cos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {f' : E βL[β] β} {x : E} (hf : HasFDerivAt f f' x) : HasFDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) β’ f') x - HasStrictFDerivAt.cos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {f' : E βL[β] β} {x : E} (hf : HasStrictFDerivAt f f' x) : HasStrictFDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) β’ f') x - HasFDerivWithinAt.sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {f' : E βL[β] β} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt (fun x => Real.sin (f x)) (Real.cos (f x) β’ f') s x - HasFDerivWithinAt.cos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {f' : E βL[β] β} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt (fun x => Real.cos (f x)) (-Real.sin (f x) β’ f') s x - fderiv_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {x : E} (hc : DifferentiableAt β f x) : fderiv β (fun x => Real.sin (f x)) x = Real.cos (f x) β’ fderiv β f x - fderiv_cos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {x : E} (hc : DifferentiableAt β f x) : fderiv β (fun x => Real.cos (f x)) x = -Real.sin (f x) β’ fderiv β f x - fderivWithin_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {x : E} {s : Set E} (hf : DifferentiableWithinAt β f s x) (hxs : UniqueDiffWithinAt β s x) : fderivWithin β (fun x => Real.sin (f x)) s x = Real.cos (f x) β’ fderivWithin β f s x - fderivWithin_cos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {x : E} {s : Set E} (hf : DifferentiableWithinAt β f s x) (hxs : UniqueDiffWithinAt β s x) : fderivWithin β (fun x => Real.cos (f x)) s x = -Real.sin (f x) β’ fderivWithin β f s x - Real.hasStrictDerivAt_const_rpow_of_neg π Mathlib.Analysis.SpecialFunctions.Pow.Deriv
{a x : β} (ha : a < 0) : HasStrictDerivAt (fun x => a ^ x) (a ^ x * Real.log a - Real.exp (Real.log a * x) * Real.sin (x * Real.pi) * Real.pi) x - Real.hasStrictFDerivAt_rpow_of_neg π Mathlib.Analysis.SpecialFunctions.Pow.Deriv
(p : β Γ β) (hp : p.1 < 0) : HasStrictFDerivAt (fun x => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) β’ ContinuousLinearMap.fst β β β + (p.1 ^ p.2 * Real.log p.1 - Real.exp (Real.log p.1 * p.2) * Real.sin (p.2 * Real.pi) * Real.pi) β’ ContinuousLinearMap.snd β β β) p - strictConcaveOn_sin_Icc π Mathlib.Analysis.Convex.SpecificFunctions.Deriv
: StrictConcaveOn β (Set.Icc 0 Real.pi) Real.sin - Real.sin_eq_one_iff π Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
{x : β} : Real.sin x = 1 β β k, Real.pi / 2 + βk * (2 * Real.pi) = x - Real.sin_eq_neg_one_iff π Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
{x : β} : Real.sin x = -1 β β k, -(Real.pi / 2) + βk * (2 * Real.pi) = x - Real.sin_eq_sin_iff π Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
{x y : β} : Real.sin x = Real.sin y β β k, y = 2 * βk * Real.pi + x β¨ y = (2 * βk + 1) * Real.pi - x - Real.sin_arctan π Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
(x : β) : Real.sin (Real.arctan x) = x / β(1 + x ^ 2) - Real.abs_sin_le_abs π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} : |Real.sin x| β€ |x| - Real.le_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} (hx : x β€ 0) : x β€ Real.sin x - Real.lt_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} (hx : x < 0) : x < Real.sin x - Real.sin_le π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} (hx : 0 β€ x) : Real.sin x β€ x - Real.sin_lt π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} (h : 0 < x) : Real.sin x < x - Real.abs_sin_lt_abs π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} (hx : x β 0) : |Real.sin x| < |x| - Real.sin_sq_le_sq π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} : Real.sin x ^ 2 β€ x ^ 2 - Real.sin_sq_lt_sq π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} (hx : x β 0) : Real.sin x ^ 2 < x ^ 2 - Real.le_sin_mul π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} (hx : 0 β€ x) (hx' : x β€ 1) : x β€ Real.sin (Real.pi / 2 * x) - Real.lt_sin_mul π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} (hx : 0 < x) (hx' : x < 1) : x < Real.sin (Real.pi / 2 * x) - Real.sin_gt_sub_cube π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} (h : 0 < x) (h' : x β€ 1) : x - x ^ 3 / 4 < Real.sin x - Real.mul_le_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} (hx : 0 β€ x) (hx' : x β€ Real.pi / 2) : 2 / Real.pi * x β€ Real.sin x - Real.mul_lt_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} (hx : 0 < x) (hx' : x < Real.pi / 2) : 2 / Real.pi * x < Real.sin x - Real.two_div_pi_mul_le_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} (hx : 0 β€ x) (hx' : x β€ Real.pi / 2) : 2 / Real.pi * x β€ Real.sin x - Real.mul_abs_le_abs_sin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} (hx : |x| β€ Real.pi / 2) : 2 / Real.pi * |x| β€ |Real.sin x| - Real.sin_le_mul π Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
{x : β} (hx : -(Real.pi / 2) β€ x) (hxβ : x β€ 0) : Real.sin x β€ 2 / Real.pi * x
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try the
#loogle command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
πReal.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
π"differ"
finds all lemmas that have"differ"somewhere in their lemma name.By subexpression:
π_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
πReal.sqrt ?a * Real.sqrt ?aIf the pattern has parameters, they are matched in any order. Both of these will find
List.map:
π(?a -> ?b) -> List ?a -> List ?b
πList ?a -> (?a -> ?b) -> List ?bBy main conclusion:
π|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of allβandβ) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
π|- _ < _ β tsum _ < tsum _
will findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
π Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ β _
woould find all lemmas which mention the constants Real.sin
and tsum, have "two" as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _ (if
there were any such lemmas). Metavariables (?a) are
assigned independently in each filter.
The #lucky button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.
This is Loogle revision 4e1aab0 serving mathlib revision 79ca167