Loogle!
Result
Found 251 definitions mentioning Real.sin. Of these, only the first 200 are shown.
- Real.sin Mathlib.Data.Complex.Exponential
ℝ → ℝ - Complex.ofReal_sin Mathlib.Data.Complex.Exponential
∀ (x : ℝ), ↑x.sin = (↑x).sin - Complex.sin_ofReal_re Mathlib.Data.Complex.Exponential
∀ (x : ℝ), (↑x).sin.re = x.sin - Real.sin_le_one Mathlib.Data.Complex.Exponential
∀ (x : ℝ), x.sin ≤ 1 - Real.sin_neg Mathlib.Data.Complex.Exponential
∀ (x : ℝ), (-x).sin = -x.sin - Real.neg_one_le_sin Mathlib.Data.Complex.Exponential
∀ (x : ℝ), -1 ≤ x.sin - Real.sin_zero Mathlib.Data.Complex.Exponential
Real.sin 0 = 0 - Real.abs_sin_le_one Mathlib.Data.Complex.Exponential
∀ (x : ℝ), |x.sin| ≤ 1 - Complex.exp_ofReal_mul_I_im Mathlib.Data.Complex.Exponential
∀ (x : ℝ), (↑x * Complex.I).exp.im = x.sin - Real.tan_eq_sin_div_cos Mathlib.Data.Complex.Exponential
∀ (x : ℝ), x.tan = x.sin / x.cos - Complex.exp_im Mathlib.Data.Complex.Exponential
∀ (x : ℂ), x.exp.im = x.re.exp * x.im.sin - Real.tan_mul_cos Mathlib.Data.Complex.Exponential
∀ {x : ℝ}, x.cos ≠ 0 → x.tan * x.cos = x.sin - Real.sin_sq_le_one Mathlib.Data.Complex.Exponential
∀ (x : ℝ), x.sin ^ 2 ≤ 1 - Real.sin_pos_of_pos_of_le_one Mathlib.Data.Complex.Exponential
∀ {x : ℝ}, 0 < x → x ≤ 1 → 0 < x.sin - Real.sin_pos_of_pos_of_le_two Mathlib.Data.Complex.Exponential
∀ {x : ℝ}, 0 < x → x ≤ 2 → 0 < x.sin - Real.abs_cos_eq_sqrt_one_sub_sin_sq Mathlib.Data.Complex.Exponential
∀ (x : ℝ), |x.cos| = (1 - x.sin ^ 2).sqrt - Real.abs_sin_eq_sqrt_one_sub_cos_sq Mathlib.Data.Complex.Exponential
∀ (x : ℝ), |x.sin| = (1 - x.cos ^ 2).sqrt - Real.cos_add Mathlib.Data.Complex.Exponential
∀ (x y : ℝ), (x + y).cos = x.cos * y.cos - x.sin * y.sin - Real.cos_sub Mathlib.Data.Complex.Exponential
∀ (x y : ℝ), (x - y).cos = x.cos * y.cos + x.sin * y.sin - Real.sin_add Mathlib.Data.Complex.Exponential
∀ (x y : ℝ), (x + y).sin = x.sin * y.cos + x.cos * y.sin - Real.sin_sub Mathlib.Data.Complex.Exponential
∀ (x y : ℝ), (x - y).sin = x.sin * y.cos - x.cos * y.sin - Real.cos_sq' Mathlib.Data.Complex.Exponential
∀ (x : ℝ), x.cos ^ 2 = 1 - x.sin ^ 2 - Real.cos_sq_add_sin_sq Mathlib.Data.Complex.Exponential
∀ (x : ℝ), x.cos ^ 2 + x.sin ^ 2 = 1 - Real.sin_sq Mathlib.Data.Complex.Exponential
∀ (x : ℝ), x.sin ^ 2 = 1 - x.cos ^ 2 - Real.sin_sq_add_cos_sq Mathlib.Data.Complex.Exponential
∀ (x : ℝ), x.sin ^ 2 + x.cos ^ 2 = 1 - Real.sin_two_mul Mathlib.Data.Complex.Exponential
∀ (x : ℝ), (2 * x).sin = 2 * x.sin * x.cos - Real.tan_div_sqrt_one_add_tan_sq Mathlib.Data.Complex.Exponential
∀ {x : ℝ}, 0 < x.cos → x.tan / (1 + x.tan ^ 2).sqrt = x.sin - Real.cos_two_mul' Mathlib.Data.Complex.Exponential
∀ (x : ℝ), (2 * x).cos = x.cos ^ 2 - x.sin ^ 2 - Real.tan_sq_div_one_add_tan_sq Mathlib.Data.Complex.Exponential
∀ {x : ℝ}, x.cos ≠ 0 → x.tan ^ 2 / (1 + x.tan ^ 2) = x.sin ^ 2 - Real.sin_three_mul Mathlib.Data.Complex.Exponential
∀ (x : ℝ), (3 * x).sin = 3 * x.sin - 4 * x.sin ^ 3 - Real.sin_sq_eq_half_sub Mathlib.Data.Complex.Exponential
∀ (x : ℝ), x.sin ^ 2 = 1 / 2 - (2 * x).cos / 2 - Real.sin_sub_sin Mathlib.Data.Complex.Exponential
∀ (x y : ℝ), x.sin - y.sin = 2 * ((x - y) / 2).sin * ((x + y) / 2).cos - Real.cos_sub_cos Mathlib.Data.Complex.Exponential
∀ (x y : ℝ), x.cos - y.cos = -2 * ((x + y) / 2).sin * ((x - y) / 2).sin - Real.sin_bound Mathlib.Data.Complex.Exponential
∀ {x : ℝ}, |x| ≤ 1 → |x.sin - (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.pi.sin = 0 - Real.continuous_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Continuous Real.sin - Real.sin_pi_sub Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ), (Real.pi - x).sin = x.sin - Real.continuousOn_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {s : Set ℝ}, ContinuousOn Real.sin s - Real.sin_add_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ), (x + Real.pi).sin = -x.sin - Real.sin_sub_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ), (x - Real.pi).sin = -x.sin - Real.sin_int_mul_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (n : ℤ), (↑n * Real.pi).sin = 0 - Real.sin_nat_mul_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (n : ℕ), (↑n * Real.pi).sin = 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 : ℝ), x.sin ∈ Set.Icc (-1) 1 - Real.sin_nonneg_of_nonneg_of_le_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, 0 ≤ x → x ≤ Real.pi → 0 ≤ x.sin - Real.sin_pos_of_pos_of_lt_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, 0 < x → x < Real.pi → 0 < x.sin - Real.sin_ne_zero_iff Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, x.sin ≠ 0 ↔ ∀ (n : ℤ), ↑n * Real.pi ≠ x - Real.sin_nonneg_of_mem_Icc Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, x ∈ Set.Icc 0 Real.pi → 0 ≤ x.sin - Real.sin_pos_of_mem_Ioo Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, x ∈ Set.Ioo 0 Real.pi → 0 < x.sin - Real.sin_eq_zero_iff Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, x.sin = 0 ↔ ∃ n, ↑n * Real.pi = x - Real.sin_neg_of_neg_of_neg_pi_lt Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, x < 0 → -Real.pi < x → x.sin < 0 - Real.sin_nonpos_of_nonnpos_of_neg_pi_le Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, x ≤ 0 → -Real.pi ≤ x → x.sin ≤ 0 - Real.sin_two_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(2 * Real.pi).sin = 0 - Real.sin_pi_div_two Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(Real.pi / 2).sin = 1 - Real.sin_eq_zero_iff_of_lt_of_lt Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, -Real.pi < x → x < Real.pi → (x.sin = 0 ↔ x = 0) - Real.sin_add_two_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ), (x + 2 * Real.pi).sin = x.sin - Real.sin_sub_two_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ), (x - 2 * Real.pi).sin = x.sin - Real.sin_eq_zero_iff_cos_eq Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, x.sin = 0 ↔ x.cos = 1 ∨ x.cos = -1 - Real.cos_pi_div_two_sub Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ), (Real.pi / 2 - x).cos = x.sin - Real.cos_sub_pi_div_two Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ), (x - Real.pi / 2).cos = x.sin - Real.sin_add_pi_div_two Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ), (x + Real.pi / 2).sin = x.cos - Real.sin_pi_div_two_sub Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ), (Real.pi / 2 - x).sin = x.cos - Real.sin_two_pi_sub Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ), (2 * Real.pi - x).sin = -x.sin - Real.cos_add_pi_div_two Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ), (x + Real.pi / 2).cos = -x.sin - Real.sin_sub_pi_div_two Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ), (x - Real.pi / 2).sin = -x.cos - Real.sin_add_int_mul_two_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ) (n : ℤ), (x + ↑n * (2 * Real.pi)).sin = x.sin - Real.sin_add_nat_mul_two_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ) (n : ℕ), (x + ↑n * (2 * Real.pi)).sin = x.sin - Real.sin_sub_int_mul_two_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ) (n : ℤ), (x - ↑n * (2 * Real.pi)).sin = x.sin - Real.sin_sub_nat_mul_two_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ) (n : ℕ), (x - ↑n * (2 * Real.pi)).sin = x.sin - Real.sin_int_mul_two_pi_sub Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ) (n : ℤ), (↑n * (2 * Real.pi) - x).sin = -x.sin - Real.sin_nat_mul_two_pi_sub Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ) (n : ℕ), (↑n * (2 * Real.pi) - x).sin = -x.sin - Real.sin_eq_sqrt_one_sub_cos_sq Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, 0 ≤ x → x ≤ Real.pi → x.sin = (1 - x.cos ^ 2).sqrt - Real.sin_add_int_mul_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ) (n : ℤ), (x + ↑n * Real.pi).sin = (-1) ^ n * x.sin - Real.sin_add_nat_mul_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ) (n : ℕ), (x + ↑n * Real.pi).sin = (-1) ^ n * x.sin - Real.sin_pi_div_six Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(Real.pi / 6).sin = 1 / 2 - Real.sin_sub_int_mul_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ) (n : ℤ), (x - ↑n * Real.pi).sin = (-1) ^ n * x.sin - Real.sin_sub_nat_mul_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ) (n : ℕ), (x - ↑n * Real.pi).sin = (-1) ^ n * x.sin - 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 : ℤ), (↑n * Real.pi - x).sin = -((-1) ^ n * x.sin) - Real.sin_nat_mul_pi_sub Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ) (n : ℕ), (↑n * Real.pi - x).sin = -((-1) ^ n * x.sin) - 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.pi / 4).sin = √2 / 2 - Real.sin_pi_div_three Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(Real.pi / 3).sin = √3 / 2 - Real.abs_sin_half Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ℝ), |(x / 2).sin| = ((1 - x.cos) / 2).sqrt - Real.sin_le_sin_of_le_of_le_pi_div_two Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x y : ℝ}, -(Real.pi / 2) ≤ x → y ≤ Real.pi / 2 → x ≤ y → x.sin ≤ y.sin - Real.sin_lt_sin_of_lt_of_le_pi_div_two Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x y : ℝ}, -(Real.pi / 2) ≤ x → y ≤ Real.pi / 2 → x < y → x.sin < y.sin - 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.pi / 3).sin ^ 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.pi / 8).sin = (2 - √2).sqrt / 2 - Real.cos_eq_sqrt_one_sub_sin_sq Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, -(Real.pi / 2) ≤ x → x ≤ Real.pi / 2 → x.cos = (1 - x.sin ^ 2).sqrt - Real.sin_half_eq_sqrt Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, 0 ≤ x → x ≤ 2 * Real.pi → (x / 2).sin = ((1 - x.cos) / 2).sqrt - Real.sin_pi_over_two_pow_succ Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (n : ℕ), (Real.pi / 2 ^ (n + 2)).sin = (2 - Real.sqrtTwoAddSeries 0 n).sqrt / 2 - Real.sin_pi_div_sixteen Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(Real.pi / 16).sin = (2 - (2 + √2).sqrt).sqrt / 2 - Real.sin_half_eq_neg_sqrt Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, -(2 * Real.pi) ≤ x → x ≤ 0 → (x / 2).sin = -((1 - x.cos) / 2).sqrt - Real.sin_sq_pi_over_two_pow Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (n : ℕ), (Real.pi / 2 ^ (n + 1)).sin ^ 2 = 1 - (Real.sqrtTwoAddSeries 0 n / 2) ^ 2 - Real.sin_pi_div_thirty_two Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(Real.pi / 32).sin = (2 - (2 + (2 + √2).sqrt).sqrt).sqrt / 2 - Real.sin_sq_pi_over_two_pow_succ Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (n : ℕ), (Real.pi / 2 ^ (n + 2)).sin ^ 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) = (↑x).sin - Real.sinOrderIso_apply Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ (x : ↑(Set.Icc (-(Real.pi / 2)) (Real.pi / 2))), Real.sinOrderIso x = ⟨(↑x).sin, ⋯⟩ - Real.Angle.sin_coe Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
∀ (x : ℝ), (↑x).sin = x.sin - Real.Angle.sin_toReal Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
∀ (θ : Real.Angle), θ.toReal.sin = θ.sin - Real.Angle.cos_sin_inj Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
∀ {θ ψ : ℝ}, θ.cos = ψ.cos → θ.sin = ψ.sin → ↑θ = ↑ψ - Real.Angle.sin_eq_real_sin_iff_eq_or_add_eq_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
∀ {θ : Real.Angle} {ψ : ℝ}, θ.sin = ψ.sin ↔ θ = ↑ψ ∨ θ + ↑ψ = ↑Real.pi - Real.Angle.sin_eq_iff_coe_eq_or_add_eq_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
∀ {θ ψ : ℝ}, θ.sin = ψ.sin ↔ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑Real.pi - Real.sin_arcsin Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ {x : ℝ}, -1 ≤ x → x ≤ 1 → x.arcsin.sin = x - Real.sin_arcsin' Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ {x : ℝ}, x ∈ Set.Icc (-1) 1 → x.arcsin.sin = x - Real.sin_arccos Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ (x : ℝ), x.arccos.sin = (1 - x ^ 2).sqrt - Real.arcsin_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ {x : ℝ}, -(Real.pi / 2) ≤ x → x ≤ Real.pi / 2 → x.sin.arcsin = x - Real.arcsin_sin' Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ {x : ℝ}, x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → x.sin.arcsin = x - Real.arcsin_eq_of_sin_eq Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ {x y : ℝ}, x.sin = y → x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → y.arcsin = x - Real.arcsin_eq_iff_eq_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ {x y : ℝ}, y ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2) → (x.arcsin = y ↔ x = y.sin) - Real.arcsin_le_iff_le_sin' Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ {x y : ℝ}, y ∈ Set.Ico (-(Real.pi / 2)) (Real.pi / 2) → (x.arcsin ≤ y ↔ x ≤ y.sin) - Real.arcsin_lt_iff_lt_sin' Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ {x y : ℝ}, y ∈ Set.Ioc (-(Real.pi / 2)) (Real.pi / 2) → (x.arcsin < y ↔ x < y.sin) - Real.le_arcsin_iff_sin_le' Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ {x y : ℝ}, x ∈ Set.Ioc (-(Real.pi / 2)) (Real.pi / 2) → (x ≤ y.arcsin ↔ x.sin ≤ y) - Real.lt_arcsin_iff_sin_lt' Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ {x y : ℝ}, x ∈ Set.Ico (-(Real.pi / 2)) (Real.pi / 2) → (x < y.arcsin ↔ x.sin < 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 : ℝ}, x ∈ Set.Icc (-1) 1 → y ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → (x.arcsin ≤ y ↔ x ≤ y.sin) - Real.arcsin_lt_iff_lt_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ {x y : ℝ}, x ∈ Set.Icc (-1) 1 → y ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → (x.arcsin < y ↔ x < y.sin) - Real.le_arcsin_iff_sin_le Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ {x y : ℝ}, x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → y ∈ Set.Icc (-1) 1 → (x ≤ y.arcsin ↔ x.sin ≤ y) - Real.lt_arcsin_iff_sin_lt Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ {x y : ℝ}, x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → y ∈ Set.Icc (-1) 1 → (x < y.arcsin ↔ x.sin < y) - Complex.abs_mul_sin_arg Mathlib.Analysis.SpecialFunctions.Complex.Arg
∀ (x : ℂ), Complex.abs x * x.arg.sin = x.im - Complex.sin_arg Mathlib.Analysis.SpecialFunctions.Complex.Arg
∀ (x : ℂ), x.arg.sin = x.im / Complex.abs x - Complex.cpow_ofReal_im Mathlib.Analysis.SpecialFunctions.Pow.Real
∀ (x : ℂ) (y : ℝ), (x ^ ↑y).im = Complex.abs x ^ y * (x.arg * y).sin - Complex.cpow_ofReal Mathlib.Analysis.SpecialFunctions.Pow.Real
∀ (x : ℂ) (y : ℝ), x ^ ↑y = ↑(Complex.abs x ^ y) * (↑(x.arg * y).cos + ↑(x.arg * y).sin * 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 : α → ℝ}, Measurable f → Measurable fun x => (f x).sin - 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 x.cos x - Real.hasStrictDerivAt_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ (x : ℝ), HasStrictDerivAt Real.sin x.cos x - Real.hasDerivAt_cos Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ (x : ℝ), HasDerivAt Real.cos (-x.sin) x - Real.hasStrictDerivAt_cos Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ (x : ℝ), HasStrictDerivAt Real.cos (-x.sin) x - Real.deriv_cos Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {x : ℝ}, deriv Real.cos x = -x.sin - Real.deriv_cos' Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
deriv Real.cos = fun x => -x.sin - 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} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ}, Differentiable ℝ f → Differentiable ℝ fun x => (f x).sin - HasDerivAt.sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {f : ℝ → ℝ} {f' x : ℝ}, HasDerivAt f f' x → HasDerivAt (fun x => (f x).sin) ((f x).cos * f') x - HasStrictDerivAt.sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {f : ℝ → ℝ} {f' x : ℝ}, HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => (f x).sin) ((f x).cos * f') x - ContDiff.sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {n : ℕ∞}, ContDiff ℝ n f → ContDiff ℝ n fun x => (f x).sin - DifferentiableAt.sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E}, DifferentiableAt ℝ f x → DifferentiableAt ℝ (fun x => (f x).sin) x - HasDerivAt.cos Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {f : ℝ → ℝ} {f' x : ℝ}, HasDerivAt f f' x → HasDerivAt (fun x => (f x).cos) (-(f x).sin * f') x - HasStrictDerivAt.cos Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {f : ℝ → ℝ} {f' x : ℝ}, HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => (f x).cos) (-(f x).sin * f') x - DifferentiableOn.sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E}, DifferentiableOn ℝ f s → DifferentiableOn ℝ (fun x => (f x).sin) s - HasDerivWithinAt.sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {f : ℝ → ℝ} {f' x : ℝ} {s : Set ℝ}, HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => (f x).sin) ((f x).cos * f') s x - ContDiffAt.sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {n : ℕ∞}, ContDiffAt ℝ n f x → ContDiffAt ℝ n (fun x => (f x).sin) x - ContDiffOn.sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {n : ℕ∞}, ContDiffOn ℝ n f s → ContDiffOn ℝ n (fun x => (f x).sin) s - DifferentiableWithinAt.sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E}, DifferentiableWithinAt ℝ f s x → DifferentiableWithinAt ℝ (fun x => (f x).sin) s x - HasDerivWithinAt.cos Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {f : ℝ → ℝ} {f' x : ℝ} {s : Set ℝ}, HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => (f x).cos) (-(f x).sin * f') s x - ContDiffWithinAt.sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} {n : ℕ∞}, ContDiffWithinAt ℝ n f s x → ContDiffWithinAt ℝ n (fun x => (f x).sin) s x - deriv_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {f : ℝ → ℝ} {x : ℝ}, DifferentiableAt ℝ f x → deriv (fun x => (f x).sin) x = (f x).cos * deriv f x - deriv_cos Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {f : ℝ → ℝ} {x : ℝ}, DifferentiableAt ℝ f x → deriv (fun x => (f x).cos) x = -(f x).sin * deriv f x - derivWithin_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ}, DifferentiableWithinAt ℝ f s x → UniqueDiffWithinAt ℝ s x → derivWithin (fun x => (f x).sin) s x = (f x).cos * derivWithin f s x - derivWithin_cos Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ}, DifferentiableWithinAt ℝ f s x → UniqueDiffWithinAt ℝ s x → derivWithin (fun x => (f x).cos) s x = -(f x).sin * derivWithin f s x - HasFDerivAt.sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E}, HasFDerivAt f f' x → HasFDerivAt (fun x => (f x).sin) ((f x).cos • f') x - HasStrictFDerivAt.sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E}, HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => (f x).sin) ((f x).cos • f') x - HasFDerivAt.cos Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E}, HasFDerivAt f f' x → HasFDerivAt (fun x => (f x).cos) (-(f x).sin • f') x - HasStrictFDerivAt.cos Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E}, HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => (f x).cos) (-(f x).sin • f') x - HasFDerivWithinAt.sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E} {s : Set E}, HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => (f x).sin) ((f x).cos • f') s x - HasFDerivWithinAt.cos Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E} {s : Set E}, HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => (f x).cos) (-(f x).sin • f') s x - fderiv_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E}, DifferentiableAt ℝ f x → fderiv ℝ (fun x => (f x).sin) x = (f x).cos • fderiv ℝ f x - fderiv_cos Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E}, DifferentiableAt ℝ f x → fderiv ℝ (fun x => (f x).cos) x = -(f x).sin • fderiv ℝ f x - fderivWithin_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E}, DifferentiableWithinAt ℝ f s x → UniqueDiffWithinAt ℝ s x → fderivWithin ℝ (fun x => (f x).sin) s x = (f x).cos • fderivWithin ℝ f s x - fderivWithin_cos Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E}, DifferentiableWithinAt ℝ f s x → UniqueDiffWithinAt ℝ s x → fderivWithin ℝ (fun x => (f x).cos) s x = -(f x).sin • fderivWithin ℝ f s x - Real.hasStrictDerivAt_const_rpow_of_neg Mathlib.Analysis.SpecialFunctions.Pow.Deriv
∀ {a x : ℝ}, a < 0 → HasStrictDerivAt (fun x => a ^ x) (a ^ x * a.log - (a.log * x).exp * (x * Real.pi).sin * Real.pi) x - Real.hasStrictFDerivAt_rpow_of_neg Mathlib.Analysis.SpecialFunctions.Pow.Deriv
∀ (p : ℝ × ℝ), p.1 < 0 → HasStrictFDerivAt (fun x => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * p.1.log - (p.1.log * p.2).exp * (p.2 * Real.pi).sin * Real.pi) • ContinuousLinearMap.snd ℝ ℝ ℝ) p - strictConcaveOn_sin_Icc Mathlib.Analysis.Convex.SpecificFunctions.Deriv
StrictConcaveOn ℝ (Set.Icc 0 Real.pi) Real.sin - Real.le_sin_mul Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
∀ {x : ℝ}, 0 ≤ x → x ≤ 1 → x ≤ (Real.pi / 2 * x).sin - Real.lt_sin_mul Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
∀ {x : ℝ}, 0 < x → x < 1 → x < (Real.pi / 2 * x).sin - Real.mul_le_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
∀ {x : ℝ}, 0 ≤ x → x ≤ Real.pi / 2 → 2 / Real.pi * x ≤ x.sin - Real.mul_lt_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
∀ {x : ℝ}, 0 < x → x < Real.pi / 2 → 2 / Real.pi * x < x.sin - Real.sin_eq_one_iff Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
∀ {x : ℝ}, x.sin = 1 ↔ ∃ k, Real.pi / 2 + ↑k * (2 * Real.pi) = x - Real.sin_eq_neg_one_iff Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
∀ {x : ℝ}, x.sin = -1 ↔ ∃ k, -(Real.pi / 2) + ↑k * (2 * Real.pi) = x - Real.sin_eq_sin_iff Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
∀ {x y : ℝ}, x.sin = y.sin ↔ ∃ k, y = 2 * ↑k * Real.pi + x ∨ y = (2 * ↑k + 1) * Real.pi - x - Real.sin_arctan Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
∀ (x : ℝ), x.arctan.sin = x / (1 + x ^ 2).sqrt - Real.le_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, x ≤ 0 → x ≤ x.sin - Real.lt_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, x < 0 → x < x.sin - Real.sin_le Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, 0 ≤ x → x.sin ≤ x - Real.sin_lt Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, 0 < x → x.sin < x - Real.sin_gt_sub_cube Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, 0 < x → x ≤ 1 → x - x ^ 3 / 4 < x.sin - Real.two_div_pi_mul_le_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, 0 ≤ x → x ≤ Real.pi / 2 → 2 / Real.pi * x ≤ x.sin - Real.sin_le_two_div_pi_mul Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, -(Real.pi / 2) ≤ x → x ≤ 0 → x.sin ≤ 2 / Real.pi * x - InnerProductGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V}, (InnerProductGeometry.angle x y).sin = 0 ↔ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = Real.pi - InnerProductGeometry.sin_eq_one_iff_angle_eq_pi_div_two Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V}, (InnerProductGeometry.angle x y).sin = 1 ↔ InnerProductGeometry.angle x y = Real.pi / 2 - InnerProductGeometry.sin_angle_mul_norm_mul_norm Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V), (InnerProductGeometry.angle x y).sin * (‖x‖ * ‖y‖) = (⟪x, x⟫_ℝ * ⟪y, y⟫_ℝ - ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ).sqrt - intervalIntegral.intervalIntegrable_sin Mathlib.Analysis.SpecialFunctions.Integrals
∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [inst : MeasureTheory.IsLocallyFiniteMeasure μ], IntervalIntegrable Real.sin μ a b - integral_cos Mathlib.Analysis.SpecialFunctions.Integrals
∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, x.cos = b.sin - a.sin - integral_sin Mathlib.Analysis.SpecialFunctions.Integrals
∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, x.sin = a.cos - b.cos - integral_sin_pow_antitone Mathlib.Analysis.SpecialFunctions.Integrals
Antitone fun n => ∫ (x : ℝ) in 0 ..Real.pi, x.sin ^ n - integral_sin_pow_pos Mathlib.Analysis.SpecialFunctions.Integrals
∀ (n : ℕ), 0 < ∫ (x : ℝ) in 0 ..Real.pi, x.sin ^ n - integral_sin_pow_succ_le Mathlib.Analysis.SpecialFunctions.Integrals
∀ (n : ℕ), ∫ (x : ℝ) in 0 ..Real.pi, x.sin ^ (n + 1) ≤ ∫ (x : ℝ) in 0 ..Real.pi, x.sin ^ n - integral_cos_sq_sub_sin_sq Mathlib.Analysis.SpecialFunctions.Integrals
∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, x.cos ^ 2 - x.sin ^ 2 = b.sin * b.cos - a.sin * a.cos - integral_sin_mul_cos₁ Mathlib.Analysis.SpecialFunctions.Integrals
∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, x.sin * x.cos = (b.sin ^ 2 - a.sin ^ 2) / 2
Did you maybe mean
About
Loogle searches of Lean and Mathlib definitions and theorems.
You may also want to try the CLI version, the 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 ?a
If 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 ?b
By 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_tsum
even though the hypothesisf i < g i
is 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 currently provided by Joachim Breitner <mail@joachim-breitner.de>.
This is Loogle revision fa2ddf5
serving mathlib revision 1147162