Loogle!
Result
Found 265 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 : ℝ), ↑(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 : ℝ}, 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 : ℝ}, 0 < x → x ≤ 1 → 0 < Real.sin x - Real.sin_pos_of_pos_of_le_two Mathlib.Data.Complex.Exponential
∀ {x : ℝ}, 0 < x → 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 : ℝ}, 0 < Real.cos x → Real.tan x / √(1 + Real.tan x ^ 2) = Real.sin x - 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 : ℝ}, 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 : ℝ}, |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 : ℝ}, 0 ≤ x → x ≤ Real.pi → 0 ≤ Real.sin x - Real.sin_pos_of_pos_of_lt_pi Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, 0 < x → 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 : ℝ}, x ∈ Set.Icc 0 Real.pi → 0 ≤ Real.sin x - Real.sin_pos_of_mem_Ioo Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, 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 : ℝ}, x < 0 → -Real.pi < x → Real.sin x < 0 - Real.sin_nonpos_of_nonnpos_of_neg_pi_le Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, x ≤ 0 → -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 : ℝ}, -Real.pi < x → 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 : ℝ}, 0 ≤ x → 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 : ℝ}, -(Real.pi / 2) ≤ x → y ≤ Real.pi / 2 → 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 : ℝ}, -(Real.pi / 2) ≤ x → y ≤ Real.pi / 2 → 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 : ℝ}, -(Real.pi / 2) ≤ x → x ≤ Real.pi / 2 → Real.cos x = √(1 - Real.sin x ^ 2) - Real.sin_half_eq_sqrt Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
∀ {x : ℝ}, 0 ≤ x → 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 : ℝ}, -(2 * Real.pi) ≤ x → 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
∀ {θ ψ : ℝ}, Real.cos θ = Real.cos ψ → 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 : ℝ}, -1 ≤ x → x ≤ 1 → Real.sin (Real.arcsin x) = x - Real.sin_arcsin' Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ {x : ℝ}, 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 : ℝ}, -(Real.pi / 2) ≤ x → x ≤ Real.pi / 2 → Real.arcsin (Real.sin x) = x - Real.arcsin_sin' Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
∀ {x : ℝ}, 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 : ℝ}, Real.sin x = y → 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 : ℝ}, 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 : ℝ}, 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 : ℝ}, 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 : ℝ}, 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 : ℝ}, 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 : ℝ}, x ∈ Set.Icc (-1) 1 → 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 : ℝ}, x ∈ Set.Icc (-1) 1 → 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 : ℝ}, x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → 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 : ℝ}, x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → 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 : α → ℝ}, 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} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ}, Differentiable ℝ f → Differentiable ℝ fun x => Real.sin (f x) - HasDerivAt.sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {f : ℝ → ℝ} {f' x : ℝ}, 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 : ℝ}, 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} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {n : ℕ∞}, ContDiff ℝ n f → ContDiff ℝ n fun x => Real.sin (f x) - 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 => Real.sin (f x)) x - HasDerivAt.cos Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {f : ℝ → ℝ} {f' x : ℝ}, 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 : ℝ}, 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} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E}, DifferentiableOn ℝ f s → DifferentiableOn ℝ (fun x => Real.sin (f x)) s - HasDerivWithinAt.sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {f : ℝ → ℝ} {f' x : ℝ} {s : Set ℝ}, 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} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {n : ℕ∞}, ContDiffAt ℝ n f x → ContDiffAt ℝ n (fun x => Real.sin (f x)) 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 => Real.sin (f x)) 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 => Real.sin (f x)) s x - HasDerivWithinAt.cos Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {f : ℝ → ℝ} {f' x : ℝ} {s : Set ℝ}, 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} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} {n : ℕ∞}, ContDiffWithinAt ℝ n f s x → ContDiffWithinAt ℝ n (fun x => Real.sin (f x)) s x - deriv_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
∀ {f : ℝ → ℝ} {x : ℝ}, 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 : ℝ}, 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 ℝ}, DifferentiableWithinAt ℝ f s x → 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 ℝ}, DifferentiableWithinAt ℝ f s x → 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} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E}, 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} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E}, 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} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E}, 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} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E}, 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} [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 => Real.sin (f x)) (Real.cos (f x) • 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 => Real.cos (f x)) (-Real.sin (f x) • 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 => Real.sin (f x)) x = Real.cos (f x) • 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 => Real.cos (f x)) x = -Real.sin (f x) • 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 => 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} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E}, DifferentiableWithinAt ℝ f s x → 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 : ℝ}, 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 : ℝ × ℝ), 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 : ℝ}, x ≤ 0 → x ≤ Real.sin x - Real.lt_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, x < 0 → x < Real.sin x - Real.sin_le Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, 0 ≤ x → Real.sin x ≤ x - Real.sin_lt Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, 0 < x → Real.sin x < x - Real.abs_sin_lt_abs Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, 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 : ℝ}, x ≠ 0 → Real.sin x ^ 2 < x ^ 2 - Real.le_sin_mul Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, 0 ≤ x → x ≤ 1 → x ≤ Real.sin (Real.pi / 2 * x) - Real.lt_sin_mul Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, 0 < x → x < 1 → x < Real.sin (Real.pi / 2 * x) - Real.sin_gt_sub_cube Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, 0 < x → x ≤ 1 → x - x ^ 3 / 4 < Real.sin x - Real.mul_le_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, 0 ≤ x → x ≤ Real.pi / 2 → 2 / Real.pi * x ≤ Real.sin x - Real.mul_lt_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, 0 < x → x < Real.pi / 2 → 2 / Real.pi * x < Real.sin x - Real.two_div_pi_mul_le_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, 0 ≤ x → x ≤ Real.pi / 2 → 2 / Real.pi * x ≤ Real.sin x - Real.mul_abs_le_abs_sin Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, |x| ≤ Real.pi / 2 → 2 / Real.pi * |x| ≤ |Real.sin x| - Real.sin_le_mul Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, -(Real.pi / 2) ≤ x → x ≤ 0 → Real.sin x ≤ 2 / Real.pi * x - Real.sin_le_two_div_pi_mul Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
∀ {x : ℝ}, -(Real.pi / 2) ≤ x → x ≤ 0 → Real.sin x ≤ 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}, Real.sin (InnerProductGeometry.angle x y) = 0 ↔ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = Real.pi
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from witin the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try 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 ?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 provided by the Lean FRO.
This is Loogle revision f46663a
serving mathlib revision c9428b0