Loogle!
Result
Found 387 declarations mentioning Real.sqrt. Of these, only the first 200 are shown.
- Real.sqrt π Mathlib.Analysis.Real.Sqrt
(x : β) : β - Real.sqrt_monotone π Mathlib.Analysis.Real.Sqrt
: Monotone Real.sqrt - Real.sqrt_nonneg π Mathlib.Analysis.Real.Sqrt
(x : β) : 0 β€ βx - Real.tendsto_sqrt_atTop π Mathlib.Analysis.Real.Sqrt
: Filter.Tendsto (fun x => βx) Filter.atTop Filter.atTop - Real.sqrt_inv π Mathlib.Analysis.Real.Sqrt
(x : β) : βxβ»ΒΉ = (βx)β»ΒΉ - Real.nat_sqrt_le_real_sqrt π Mathlib.Analysis.Real.Sqrt
{a : β} : βa.sqrt β€ ββa - Real.sqrt_le_sqrt π Mathlib.Analysis.Real.Sqrt
{x y : β} (h : x β€ y) : βx β€ βy - Real.comap_sqrt_atTop π Mathlib.Analysis.Real.Sqrt
: Filter.comap (fun x => βx) Filter.atTop = Filter.atTop - Real.map_sqrt_atTop π Mathlib.Analysis.Real.Sqrt
: Filter.map (fun x => βx) Filter.atTop = Filter.atTop - Real.sqrt_one π Mathlib.Analysis.Real.Sqrt
: β1 = 1 - Real.sqrt_zero π Mathlib.Analysis.Real.Sqrt
: β0 = 0 - Real.strictMonoOn_sqrt π Mathlib.Analysis.Real.Sqrt
: StrictMonoOn Real.sqrt (Set.Ici 0) - Real.continuous_sqrt π Mathlib.Analysis.Real.Sqrt
: Continuous fun x => βx - Real.div_sqrt π Mathlib.Analysis.Real.Sqrt
{x : β} : x / βx = βx - Real.floor_real_sqrt_eq_nat_sqrt π Mathlib.Analysis.Real.Sqrt
{a : β} : βββaβ = βa.sqrt - Real.le_sqrt_self_iff π Mathlib.Analysis.Real.Sqrt
{x : β} : x β€ βx β x β€ 1 - Real.sqrt_lt_self_iff π Mathlib.Analysis.Real.Sqrt
{x : β} : βx < x β 1 < x - Real.sqrt_mul_self_eq_abs π Mathlib.Analysis.Real.Sqrt
(x : β) : β(x * x) = |x| - Real.nat_floor_real_sqrt_eq_nat_sqrt π Mathlib.Analysis.Real.Sqrt
{a : β} : βββaββ = a.sqrt - Real.sqrt_div_self π Mathlib.Analysis.Real.Sqrt
{x : β} : βx / x = (βx)β»ΒΉ - Real.sqrt_eq_one π Mathlib.Analysis.Real.Sqrt
{x : β} : βx = 1 β x = 1 - Real.sqrt_eq_zero_of_nonpos π Mathlib.Analysis.Real.Sqrt
{x : β} (h : x β€ 0) : βx = 0 - Real.sqrt_eq_zero' π Mathlib.Analysis.Real.Sqrt
{x : β} : βx = 0 β x β€ 0 - Real.sqrt_ne_zero' π Mathlib.Analysis.Real.Sqrt
{x : β} : βx β 0 β 0 < x - Real.sqrt_pos_of_pos π Mathlib.Analysis.Real.Sqrt
{x : β} : 0 < x β 0 < βx - Real.one_le_sqrt π Mathlib.Analysis.Real.Sqrt
{x : β} : 1 β€ βx β 1 β€ x - Real.sqrt_le_one π Mathlib.Analysis.Real.Sqrt
{x : β} : βx β€ 1 β x β€ 1 - Real.sqrt_pos π Mathlib.Analysis.Real.Sqrt
{x : β} : 0 < βx β 0 < x - Real.sqrt_lt_sqrt π Mathlib.Analysis.Real.Sqrt
{x y : β} (hx : 0 β€ x) (h : x < y) : βx < βy - Real.sqrt_mul_self π Mathlib.Analysis.Real.Sqrt
{x : β} (h : 0 β€ x) : β(x * x) = x - Real.mul_self_sqrt π Mathlib.Analysis.Real.Sqrt
{x : β} (h : 0 β€ x) : βx * βx = x - Real.sqrt_le_sqrt_iff π Mathlib.Analysis.Real.Sqrt
{x y : β} (hy : 0 β€ y) : βx β€ βy β x β€ y - Real.sqrt_le_sqrt_iff' π Mathlib.Analysis.Real.Sqrt
{x y : β} (hx : 0 < x) : βx β€ βy β x β€ y - Real.sqrt_lt_sqrt_iff π Mathlib.Analysis.Real.Sqrt
{x y : β} (hx : 0 β€ x) : βx < βy β x < y - Real.sqrt_lt_sqrt_iff_of_pos π Mathlib.Analysis.Real.Sqrt
{x y : β} (hy : 0 < y) : βx < βy β x < y - Real.real_sqrt_le_nat_sqrt_succ π Mathlib.Analysis.Real.Sqrt
{a : β} : ββa β€ βa.sqrt + 1 - Real.real_sqrt_lt_nat_sqrt_succ π Mathlib.Analysis.Real.Sqrt
{a : β} : ββa < βa.sqrt + 1 - Real.sqrt_sq_eq_abs π Mathlib.Analysis.Real.Sqrt
(x : β) : β(x ^ 2) = |x| - Continuous.sqrt π Mathlib.Analysis.Real.Sqrt
{Ξ± : Type u_1} [TopologicalSpace Ξ±] {f : Ξ± β β} (h : Continuous f) : Continuous fun x => β(f x) - Real.lt_sqrt_self_iff π Mathlib.Analysis.Real.Sqrt
{x : β} : x < βx β x β 0 β§ x < 1 - Real.sqrt_le_self_iff π Mathlib.Analysis.Real.Sqrt
{x : β} : βx β€ x β x = 0 β¨ 1 β€ x - Real.one_lt_sqrt_two π Mathlib.Analysis.Real.Sqrt
: 1 < β2 - Real.le_sqrt_of_sq_le π Mathlib.Analysis.Real.Sqrt
{x y : β} (h : x ^ 2 β€ y) : x β€ βy - Real.lt_sq_of_sqrt_lt π Mathlib.Analysis.Real.Sqrt
{x y : β} (h : βx < y) : x < y ^ 2 - Real.lt_sqrt_of_sq_lt π Mathlib.Analysis.Real.Sqrt
{x y : β} (h : x ^ 2 < y) : x < βy - Real.sqrt_eq_iff_mul_self_eq_of_pos π Mathlib.Analysis.Real.Sqrt
{x y : β} (h : 0 < y) : βx = y β y * y = x - ContinuousAt.sqrt π Mathlib.Analysis.Real.Sqrt
{Ξ± : Type u_1} [TopologicalSpace Ξ±] {f : Ξ± β β} {x : Ξ±} (h : ContinuousAt f x) : ContinuousAt (fun x => β(f x)) x - Real.sqrt_eq_zero π Mathlib.Analysis.Real.Sqrt
{x : β} (h : 0 β€ x) : βx = 0 β x = 0 - Real.sqrt_ne_zero π Mathlib.Analysis.Real.Sqrt
{x : β} (h : 0 β€ x) : βx β 0 β x β 0 - ContinuousOn.sqrt π Mathlib.Analysis.Real.Sqrt
{Ξ± : Type u_1} [TopologicalSpace Ξ±] {f : Ξ± β β} {s : Set Ξ±} (h : ContinuousOn f s) : ContinuousOn (fun x => β(f x)) s - Real.sq_sqrt' π Mathlib.Analysis.Real.Sqrt
{x : β} : βx ^ 2 = max x 0 - Real.sqrt_div_self' π Mathlib.Analysis.Real.Sqrt
{x : β} : βx / x = 1 / βx - Real.neg_sqrt_le_of_sq_le π Mathlib.Analysis.Real.Sqrt
{x y : β} (h : x ^ 2 β€ y) : -βy β€ x - Real.neg_sqrt_lt_of_sq_lt π Mathlib.Analysis.Real.Sqrt
{x y : β} (h : x ^ 2 < y) : -βy < x - Real.sq_sqrt π Mathlib.Analysis.Real.Sqrt
{x : β} (h : 0 β€ x) : βx ^ 2 = x - Real.sqrt_inj π Mathlib.Analysis.Real.Sqrt
{x y : β} (hx : 0 β€ x) (hy : 0 β€ y) : βx = βy β x = y - Real.sqrt_sq π Mathlib.Analysis.Real.Sqrt
{x : β} (h : 0 β€ x) : β(x ^ 2) = x - Real.abs_le_sqrt π Mathlib.Analysis.Real.Sqrt
{x y : β} (h : x ^ 2 β€ y) : |x| β€ βy - ContinuousWithinAt.sqrt π Mathlib.Analysis.Real.Sqrt
{Ξ± : Type u_1} [TopologicalSpace Ξ±] {f : Ξ± β β} {s : Set Ξ±} {x : Ξ±} (h : ContinuousWithinAt f s x) : ContinuousWithinAt (fun x => β(f x)) s x - Real.sqrt_mul π Mathlib.Analysis.Real.Sqrt
{x : β} (hx : 0 β€ x) (y : β) : β(x * y) = βx * βy - Real.sqrt_mul' π Mathlib.Analysis.Real.Sqrt
(x : β) {y : β} (hy : 0 β€ y) : β(x * y) = βx * βy - Filter.Tendsto.sqrt π Mathlib.Analysis.Real.Sqrt
{Ξ± : Type u_1} {f : Ξ± β β} {l : Filter Ξ±} {x : β} (h : Filter.Tendsto f l (nhds x)) : Filter.Tendsto (fun x => β(f x)) l (nhds βx) - Real.coe_sqrt π Mathlib.Analysis.Real.Sqrt
{x : NNReal} : β(NNReal.sqrt x) = ββx - Real.sqrt_div π Mathlib.Analysis.Real.Sqrt
{x : β} (hx : 0 β€ x) (y : β) : β(x / y) = βx / βy - Real.sqrt_div' π Mathlib.Analysis.Real.Sqrt
(x : β) {y : β} (hy : 0 β€ y) : β(x / y) = βx / βy - Real.sqrt_eq_iff_mul_self_eq π Mathlib.Analysis.Real.Sqrt
{x y : β} (hx : 0 β€ x) (hy : 0 β€ y) : βx = y β x = y * y - Real.le_sqrt' π Mathlib.Analysis.Real.Sqrt
{x y : β} (hx : 0 < x) : x β€ βy β x ^ 2 β€ y - Real.lt_sqrt π Mathlib.Analysis.Real.Sqrt
{x y : β} (hx : 0 β€ x) : x < βy β x ^ 2 < y - Real.sq_lt π Mathlib.Analysis.Real.Sqrt
{x y : β} : x ^ 2 < y β -βy < x β§ x < βy - Real.sqrt_le_left π Mathlib.Analysis.Real.Sqrt
{x y : β} (hy : 0 β€ y) : βx β€ y β x β€ y ^ 2 - Real.sqrt_lt' π Mathlib.Analysis.Real.Sqrt
{x y : β} (hy : 0 < y) : βx < y β x < y ^ 2 - Real.sqrt_le_iff π Mathlib.Analysis.Real.Sqrt
{x y : β} : βx β€ y β 0 β€ y β§ x β€ y ^ 2 - Real.sqrt_eq_iff_eq_sq π Mathlib.Analysis.Real.Sqrt
{x y : β} (hx : 0 β€ x) (hy : 0 β€ y) : βx = y β x = y ^ 2 - Real.sqrt_prod π Mathlib.Analysis.Real.Sqrt
{ΞΉ : Type u_1} (s : Finset ΞΉ) {x : ΞΉ β β} (hx : β i β s, 0 β€ x i) : β(β i β s, x i) = β i β s, β(x i) - Real.le_sqrt π Mathlib.Analysis.Real.Sqrt
{x y : β} (hx : 0 β€ x) (hy : 0 β€ y) : x β€ βy β x ^ 2 β€ y - Real.sq_le π Mathlib.Analysis.Real.Sqrt
{x y : β} (h : 0 β€ y) : x ^ 2 β€ y β -βy β€ x β§ x β€ βy - Real.sqrt_lt π Mathlib.Analysis.Real.Sqrt
{x y : β} (hx : 0 β€ x) (hy : 0 β€ y) : βx < y β x < y ^ 2 - Real.sqrt_eq_cases π Mathlib.Analysis.Real.Sqrt
{x y : β} : βx = y β y * y = x β§ 0 β€ y β¨ x < 0 β§ y = 0 - Real.sqrt_two_lt_three_halves π Mathlib.Analysis.Real.Sqrt
: β2 < 3 / 2 - Real.inv_sqrt_two_sub_one π Mathlib.Analysis.Real.Sqrt
: (β2 - 1)β»ΒΉ = β2 + 1 - Real.sqrt_one_add_le π Mathlib.Analysis.Real.Sqrt
{x : β} (h : -1 β€ x) : β(1 + x) β€ 1 + x / 2 - Real.sum_sqrt_mul_sqrt_le π Mathlib.Analysis.Real.Sqrt
{ΞΉ : Type u_2} {f g : ΞΉ β β} (s : Finset ΞΉ) (hf : β (i : ΞΉ), 0 β€ f i) (hg : β (i : ΞΉ), 0 β€ g i) : β i β s, β(f i) * β(g i) β€ β(β i β s, f i) * β(β i β s, g i) - Real.sum_mul_le_sqrt_mul_sqrt π Mathlib.Analysis.Real.Sqrt
{ΞΉ : Type u_2} (s : Finset ΞΉ) (f g : ΞΉ β β) : β i β s, f i * g i β€ β(β i β s, f i ^ 2) * β(β i β s, g i ^ 2) - Complex.norm_def π Mathlib.Analysis.Complex.Norm
(z : β) : βzβ = β(Complex.normSq z) - Complex.norm_le_sqrt_two_mul_max π Mathlib.Analysis.Complex.Norm
(z : β) : βzβ β€ β2 * max |z.re| |z.im| - Complex.norm_eq_sqrt_sq_add_sq π Mathlib.Analysis.Complex.Norm
(z : β) : βzβ = β(z.re ^ 2 + z.im ^ 2) - Complex.norm_add_mul_I π Mathlib.Analysis.Complex.Norm
(x y : β) : ββx + βy * Complex.Iβ = β(x ^ 2 + y ^ 2) - Complex.dist_eq_re_im π Mathlib.Analysis.Complex.Norm
(z w : β) : dist z w = β((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2) - Complex.dist_mk π Mathlib.Analysis.Complex.Norm
(xβ yβ xβ yβ : β) : dist { re := xβ, im := yβ } { re := xβ, im := yβ } = β((xβ - xβ) ^ 2 + (yβ - yβ) ^ 2) - Complex.normSq_ofReal_add_I_mul_sqrt_one_sub π Mathlib.Analysis.Complex.Norm
{x : β} (hx : βxβ β€ 1) : Complex.normSq (βx + Complex.I * ββ(1 - x ^ 2)) = 1 - Complex.normSq_ofReal_sub_I_mul_sqrt_one_sub π Mathlib.Analysis.Complex.Norm
{x : β} (hx : βxβ β€ 1) : Complex.normSq (βx - Complex.I * ββ(1 - x ^ 2)) = 1 - RCLike.sqrt_normSq_eq_norm π Mathlib.Analysis.RCLike.Basic
{K : Type u_1} [RCLike K] {z : K} : β(RCLike.normSq z) = βzβ - Real.abs_cos_eq_sqrt_one_sub_sin_sq π Mathlib.Analysis.Complex.Trigonometric
(x : β) : |Real.cos x| = β(1 - Real.sin x ^ 2) - Real.abs_sin_eq_sqrt_one_sub_cos_sq π Mathlib.Analysis.Complex.Trigonometric
(x : β) : |Real.sin x| = β(1 - Real.cos x ^ 2) - Real.inv_sqrt_one_add_tan_sq π Mathlib.Analysis.Complex.Trigonometric
{x : β} (hx : 0 < Real.cos x) : (β(1 + Real.tan x ^ 2))β»ΒΉ = Real.cos x - Real.tan_div_sqrt_one_add_tan_sq π Mathlib.Analysis.Complex.Trigonometric
{x : β} (hx : 0 < Real.cos x) : Real.tan x / β(1 + Real.tan x ^ 2) = Real.sin x - Real.exp_half π Mathlib.Analysis.SpecialFunctions.Exp
(x : β) : Real.exp (x / 2) = β(Real.exp x) - Real.sqrtTwoAddSeries_one π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.sqrtTwoAddSeries 0 1 = β2 - Real.sqrtTwoAddSeries_succ π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
(x : β) (n : β) : x.sqrtTwoAddSeries (n + 1) = (β(2 + x)).sqrtTwoAddSeries n - Real.tan_pi_div_three π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.tan (Real.pi / 3) = β3 - 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.sqrtTwoAddSeries_two π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.sqrtTwoAddSeries 0 2 = β(2 + β2) - Real.tan_pi_div_six π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.tan (Real.pi / 6) = 1 / β3 - Real.cos_pi_div_four π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.cos (Real.pi / 4) = β2 / 2 - Real.cos_pi_div_six π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.cos (Real.pi / 6) = β3 / 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.cos_half π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
{x : β} (hl : -Real.pi β€ x) (hr : x β€ Real.pi) : Real.cos (x / 2) = β((1 + Real.cos x) / 2) - Real.cos_pi_div_five π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.cos (Real.pi / 5) = (1 + β5) / 4 - 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.cos_pi_div_eight π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.cos (Real.pi / 8) = β(2 + β2) / 2 - Real.sin_pi_div_eight π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.sin (Real.pi / 8) = β(2 - β2) / 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_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.cos_pi_div_sixteen π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.cos (Real.pi / 16) = β(2 + β(2 + β2)) / 2 - Real.sin_pi_div_sixteen π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.sin (Real.pi / 16) = β(2 - β(2 + β2)) / 2 - Real.cos_pi_div_thirty_two π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.cos (Real.pi / 32) = β(2 + β(2 + β(2 + β2))) / 2 - Real.sin_pi_div_thirty_two π Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
: Real.sin (Real.pi / 32) = β(2 - β(2 + β(2 + β2))) / 2 - Real.cos_arcsin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
(x : β) : Real.cos (Real.arcsin x) = β(1 - x ^ 2) - Real.sin_arccos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
(x : β) : Real.sin (Real.arccos x) = β(1 - x ^ 2) - Real.arccos_eq_arcsin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x : β} (h : 0 β€ x) : Real.arccos x = Real.arcsin β(1 - x ^ 2) - Real.arcsin_eq_arccos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x : β} (h : 0 β€ x) : Real.arcsin x = Real.arccos β(1 - x ^ 2) - Real.tan_arccos π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
(x : β) : Real.tan (Real.arccos x) = β(1 - x ^ 2) / x - Real.tan_arcsin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
(x : β) : Real.tan (Real.arcsin x) = x / β(1 - x ^ 2) - Real.arccos_le_pi_div_four π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x : β} : Real.arccos x β€ Real.pi / 4 β β2 / 2 β€ x - Real.pi_div_four_le_arcsin π Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
{x : β} : Real.pi / 4 β€ Real.arcsin x β β2 / 2 β€ x - Real.log_sqrt π Mathlib.Analysis.SpecialFunctions.Log.Basic
{x : β} (hx : 0 β€ x) : Real.log βx = Real.log x / 2 - Real.sqrt_eq_rpow π Mathlib.Analysis.SpecialFunctions.Pow.Real
(x : β) : βx = x ^ (1 / 2) - Real.rpow_div_two_eq_sqrt π Mathlib.Analysis.SpecialFunctions.Pow.Real
{x : β} (r : β) (hx : 0 β€ x) : x ^ (r / 2) = βx ^ r - Complex.cpow_inv_two_re π Mathlib.Analysis.SpecialFunctions.Pow.Real
(x : β) : (x ^ 2β»ΒΉ).re = β((βxβ + x.re) / 2) - Complex.abs_cpow_inv_two_im π Mathlib.Analysis.SpecialFunctions.Pow.Real
(x : β) : |(x ^ 2β»ΒΉ).im| = β((βxβ - x.re) / 2) - Complex.cpow_inv_two_im_eq_sqrt π Mathlib.Analysis.SpecialFunctions.Pow.Real
{x : β} (hx : 0 β€ x.im) : (x ^ 2β»ΒΉ).im = β((βxβ - x.re) / 2) - Complex.cpow_inv_two_im_eq_neg_sqrt π Mathlib.Analysis.SpecialFunctions.Pow.Real
{x : β} (hx : x.im < 0) : (x ^ 2β»ΒΉ).im = -β((βxβ - x.re) / 2) - Asymptotics.IsBigO.sqrt π Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
{Ξ± : Type u_1} {l : Filter Ξ±} {f g : Ξ± β β} (hfg : f =O[l] g) (hg : 0 β€αΆ [l] g) : (fun x => β(f x)) =O[l] fun x => β(g x) - Asymptotics.IsLittleO.sqrt π Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
{Ξ± : Type u_1} {l : Filter Ξ±} {f g : Ξ± β β} (hfg : f =o[l] g) (hg : 0 β€αΆ [l] g) : (fun x => β(f x)) =o[l] fun x => β(g x) - Asymptotics.IsTheta.sqrt π Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
{Ξ± : Type u_1} {l : Filter Ξ±} {f g : Ξ± β β} (hfg : f =Ξ[l] g) (hf : 0 β€αΆ [l] f) (hg : 0 β€αΆ [l] g) : (fun x => β(f x)) =Ξ[l] fun x => β(g x) - Measurable.sqrt π Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
{Ξ± : Type u_1} {m : MeasurableSpace Ξ±} {f : Ξ± β β} (hf : Measurable f) : Measurable fun x => β(f x) - AEMeasurable.sqrt π Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
{Ξ± : Type u_1} {m : MeasurableSpace Ξ±} {ΞΌ : MeasureTheory.Measure Ξ±} {f : Ξ± β β} (hf : AEMeasurable f ΞΌ) : AEMeasurable (fun x => β(f x)) ΞΌ - InnerProductSpace.Core.sqrt_normSq_eq_norm π Mathlib.Analysis.InnerProductSpace.Defs
{π : Type u_1} {F : Type u_3} [RCLike π] [AddCommGroup F] [Module π F] [c : PreInnerProductSpace.Core π F] (x : F) : β(InnerProductSpace.Core.normSq x) = βxβ - InnerProductSpace.Core.norm_eq_sqrt_re_inner π Mathlib.Analysis.InnerProductSpace.Defs
{π : Type u_1} {F : Type u_3} [RCLike π] [AddCommGroup F] [Module π F] [c : PreInnerProductSpace.Core π F] (x : F) : βxβ = β(RCLike.re (inner π x x)) - norm_eq_sqrt_real_inner π Mathlib.Analysis.InnerProductSpace.Basic
{F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace β F] (x : F) : βxβ = β(inner β x x) - norm_sub_eq_sqrt_iff_real_inner_eq_zero π Mathlib.Analysis.InnerProductSpace.Basic
{F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace β F] {x y : F} : βx - yβ = β(βxβ * βxβ + βyβ * βyβ) β inner β x y = 0 - norm_add_eq_sqrt_iff_real_inner_eq_zero π Mathlib.Analysis.InnerProductSpace.Basic
{F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace β F] {x y : F} : βx + yβ = β(βxβ * βxβ + βyβ * βyβ) β inner β x y = 0 - norm_eq_sqrt_re_inner π Mathlib.Analysis.InnerProductSpace.Basic
{π : Type u_1} {E : Type u_2} [RCLike π] [SeminormedAddCommGroup E] [InnerProductSpace π E] (x : E) : βxβ = β(RCLike.re (inner π x x)) - WithLp.prod_norm_eq_of_L2 π Mathlib.Analysis.Normed.Lp.ProdLp
{Ξ± : Type u_2} {Ξ² : Type u_3} [SeminormedAddCommGroup Ξ±] [SeminormedAddCommGroup Ξ²] (x : WithLp 2 (Ξ± Γ Ξ²)) : βxβ = β(βx.fstβ ^ 2 + βx.sndβ ^ 2) - WithLp.prod_dist_eq_of_L2 π Mathlib.Analysis.Normed.Lp.ProdLp
{Ξ± : Type u_2} {Ξ² : Type u_3} [SeminormedAddCommGroup Ξ±] [SeminormedAddCommGroup Ξ²] (x y : WithLp 2 (Ξ± Γ Ξ²)) : dist x y = β(dist x.fst y.fst ^ 2 + dist x.snd y.snd ^ 2) - PiLp.norm_eq_of_L2 π Mathlib.Analysis.Normed.Lp.PiLp
{ΞΉ : Type u_2} {Ξ² : ΞΉ β Type u_4} [Fintype ΞΉ] [(i : ΞΉ) β SeminormedAddCommGroup (Ξ² i)] (x : PiLp 2 Ξ²) : βxβ = β(β i, βx.ofLp iβ ^ 2) - PiLp.dist_eq_of_L2 π Mathlib.Analysis.Normed.Lp.PiLp
{ΞΉ : Type u_2} {Ξ² : ΞΉ β Type u_4} [Fintype ΞΉ] [(i : ΞΉ) β SeminormedAddCommGroup (Ξ² i)] (x y : PiLp 2 Ξ²) : dist x y = β(β i, dist (x.ofLp i) (y.ofLp i) ^ 2) - OrthonormalBasis.norm_le_card_mul_iSup_norm_inner π Mathlib.Analysis.InnerProductSpace.PiL2
{ΞΉ : Type u_1} {π : Type u_3} [RCLike π] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace π E] [Fintype ΞΉ] (b : OrthonormalBasis ΞΉ π E) (x : E) : βxβ β€ ββ(Fintype.card ΞΉ) * β¨ i, βinner π (b i) xβ - EuclideanSpace.norm_eq π Mathlib.Analysis.InnerProductSpace.PiL2
{π : Type u_7} [RCLike π] {n : Type u_8} [Fintype n] (x : EuclideanSpace π n) : βxβ = β(β i, βx.ofLp iβ ^ 2) - EuclideanSpace.dist_eq π Mathlib.Analysis.InnerProductSpace.PiL2
{π : Type u_7} [RCLike π] {n : Type u_8} [Fintype n] (x y : EuclideanSpace π n) : dist x y = β(β i, dist (x.ofLp i) (y.ofLp i) ^ 2) - TsirelsonInequality.sqrt_two_inv_mul_self π Mathlib.Algebra.Star.CHSH
: (β2)β»ΒΉ * (β2)β»ΒΉ = 2β»ΒΉ - tsirelson_inequality π Mathlib.Algebra.Star.CHSH
{R : Type u} [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [Algebra β R] [IsOrderedModule β R] [StarModule β R] (Aβ Aβ Bβ Bβ : R) (T : IsCHSHTuple Aβ Aβ Bβ Bβ) : Aβ * Bβ + Aβ * Bβ + Aβ * Bβ - Aβ * Bβ β€ β2 ^ 3 β’ 1 - CStarAlgebra.sqrt_toReal_spectralRadius_self_mul_star_eq_norm π Mathlib.Analysis.CStarAlgebra.Spectrum
{A : Type u_1} [CStarAlgebra A] (a : A) : β(spectralRadius β (a * star a)).toReal = βaβ - CStarAlgebra.sqrt_toReal_spectralRadius_star_mul_self_eq_norm π Mathlib.Analysis.CStarAlgebra.Spectrum
{A : Type u_1} [CStarAlgebra A] (a : A) : β(spectralRadius β (star a * a)).toReal = βaβ - CFC.sqrt_eq_real_sqrt π Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
{A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module β A] [SMulCommClass β A A] [IsScalarTower β A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus β A IsSelfAdjoint] [NonnegSpectrumClass β A] [IsSemitopologicalRing A] [T2Space A] (a : A) (ha : 0 β€ a := by cfc_tac) : CFC.sqrt a = cfcβ Real.sqrt a - CFC.norm_sqrt π Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
{A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace β A] [IsScalarTower β A A] [SMulCommClass β A A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass β A] [NonUnitalIsometricContinuousFunctionalCalculus β A IsSelfAdjoint] (a : A) (ha : 0 β€ a := by cfc_tac) : βCFC.sqrt aβ = ββaβ - CStarModule.norm_eq_sqrt_norm_inner_self π Mathlib.Analysis.CStarAlgebra.Module.Defs
{A : Type u_1} {E : Type u_2} {instβ : NonUnitalSemiring A} {instβΒΉ : StarRing A} {instβΒ² : Module β A} {instβΒ³ : AddCommGroup E} {instββ΄ : Module β E} {instββ΅ : PartialOrder A} {instββΆ : SMul A E} {instββ· : Norm A} {instββΈ : Norm E} [self : CStarModule A E] (x : E) : βxβ = ββinner A x xβ - CStarModule.mk π Mathlib.Analysis.CStarAlgebra.Module.Defs
{A : Type u_1} {E : Type u_2} [NonUnitalSemiring A] [StarRing A] [Module β A] [AddCommGroup E] [Module β E] [PartialOrder A] [SMul A E] [Norm A] [Norm E] [toInner : Inner A E] (inner_add_right : β {x y z : E}, inner A x (y + z) = inner A x y + inner A x z) (inner_self_nonneg : β {x : E}, 0 β€ inner A x x) (inner_self : β {x : E}, inner A x x = 0 β x = 0) (inner_op_smul_right : β {a : A} {x y : E}, inner A x (a β’ y) = a * inner A x y) (inner_smul_right_complex : β {z : β} {x y : E}, inner A x (z β’ y) = z β’ inner A x y) (star_inner : β (x y : E), star (inner A x y) = inner A y x) (norm_eq_sqrt_norm_inner_self : β (x : E), βxβ = ββinner A x xβ) : CStarModule A E - WithCStarModule.pi_norm π Mathlib.Analysis.CStarAlgebra.Module.Constructions
{A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {ΞΉ : Type u_2} {E : ΞΉ β Type u_3} [Fintype ΞΉ] [(i : ΞΉ) β NormedAddCommGroup (E i)] [(i : ΞΉ) β Module β (E i)] [(i : ΞΉ) β SMul A (E i)] [(i : ΞΉ) β CStarModule A (E i)] (x : WithCStarModule A ((i : ΞΉ) β E i)) : βxβ = βββ i, inner A (x i) (x i)β - WithCStarModule.prod_norm π Mathlib.Analysis.CStarAlgebra.Module.Constructions
{A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [Module β E] [SMul A E] [NormedAddCommGroup F] [Module β F] [SMul A F] [CStarModule A E] [CStarModule A F] (x : WithCStarModule A (E Γ F)) : βxβ = ββinner A x.1 x.1 + inner A x.2 x.2β - ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left π Mathlib.Analysis.InnerProductSpace.Adjoint
{π : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike π] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace π E] [InnerProductSpace π F] [CompleteSpace E] [CompleteSpace F] (A : E βL[π] F) (x : E) : βA xβ = β(RCLike.re (inner π ((ContinuousLinearMap.adjoint A βSL A) x) x)) - ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right π Mathlib.Analysis.InnerProductSpace.Adjoint
{π : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike π] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace π E] [InnerProductSpace π F] [CompleteSpace E] [CompleteSpace F] (A : E βL[π] F) (x : E) : βA xβ = β(RCLike.re (inner π x ((ContinuousLinearMap.adjoint A βSL A) x))) - PositiveLinearMap.cauchy_schwarz_mul_star π Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
{A : Type u_1} [NonUnitalRing A] [PartialOrder A] [Module β A] [StarRing A] [StarOrderedRing A] [SelfAdjointDecompose A] [StarModule β A] [IsScalarTower β A A] {F : Type u_2} [FunLike F A β] [LinearMapClass F β A β] [OrderHomClass F A β] (f : F) (x y : A) : βf (x * star y)β β€ ββf (x * star x)β * ββf (y * star y)β - PositiveLinearMap.cauchy_schwarz_star_mul π Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
{A : Type u_1} [NonUnitalRing A] [PartialOrder A] [Module β A] [StarRing A] [StarOrderedRing A] [SelfAdjointDecompose A] [StarModule β A] [IsScalarTower β A A] {F : Type u_2} [FunLike F A β] [LinearMapClass F β A β] [OrderHomClass F A β] (f : F) (x y : A) : βf (star x * y)β β€ ββf (star x * x)β * ββf (star y * y)β - PositiveLinearMap.norm_map_mul_star_le π Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
{A : Type u_1} [NonUnitalRing A] [PartialOrder A] [Module β A] [StarRing A] [StarOrderedRing A] [SelfAdjointDecompose A] [StarModule β A] [IsScalarTower β A A] {F : Type u_2} [FunLike F A β] [LinearMapClass F β A β] [OrderHomClass F A β] (f : F) (x y : A) : βf (x * star y)β β€ ββf (x * star x)β * ββf (y * star y)β - PositiveLinearMap.norm_map_star_mul_le π Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
{A : Type u_1} [NonUnitalRing A] [PartialOrder A] [Module β A] [StarRing A] [StarOrderedRing A] [SelfAdjointDecompose A] [StarModule β A] [IsScalarTower β A A] {F : Type u_2} [FunLike F A β] [LinearMapClass F β A β] [OrderHomClass F A β] (f : F) (x y : A) : βf (star x * y)β β€ ββf (star x * x)β * ββf (star y * y)β - PositiveLinearMap.preGNS_norm_def π Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
{A : Type u_1} [NonUnitalRing A] [PartialOrder A] [Module β A] [StarRing A] [StarOrderedRing A] [SelfAdjointDecompose A] [StarModule β A] [IsScalarTower β A A] (f : A ββ[β] β) (a : f.PreGNS) : βaβ = β(f (star (f.ofPreGNS a) * f.ofPreGNS a)).re - PositiveLinearMap.preGNS_norm_def' π Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
{A : Type u_1} [NonUnitalRing A] [PartialOrder A] [Module β A] [StarRing A] [StarOrderedRing A] [SelfAdjointDecompose A] [StarModule β A] [IsScalarTower β A A] (f : A ββ[β] β) (a : f.PreGNS) : βaβ = ββf (star (f.ofPreGNS a) * f.ofPreGNS a)β - PositiveContinuousLinearMap.norm_map_le_sqrt_opNorm_mul π Mathlib.Analysis.CStarAlgebra.PositiveLinearFunctional
{A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (f : A βP[β] β) (x : A) : βf xβ β€ ββf.toContinuousLinearMapβ * ββf (star x * x)β - Real.contDiffAt_sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{x : β} {n : WithTop ββ} (hx : x β 0) : ContDiffAt β n (fun x => βx) x - ContDiff.sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {n : WithTop ββ} (hf : ContDiff β n f) (h : β (x : E), f x β 0) : ContDiff β n fun y => β(f y) - ContDiffAt.sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {n : WithTop ββ} {x : E} (hf : ContDiffAt β n f x) (hx : f x β 0) : ContDiffAt β n (fun y => β(f y)) x - ContDiffWithinAt.sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {n : WithTop ββ} {s : Set E} {x : E} (hf : ContDiffWithinAt β n f s x) (hx : f x β 0) : ContDiffWithinAt β n (fun y => β(f y)) s x - ContDiffOn.sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {n : WithTop ββ} {s : Set E} (hf : ContDiffOn β n f s) (hs : β x β s, f x β 0) : ContDiffOn β n (fun y => β(f y)) s - Real.hasDerivAt_sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{x : β} (hx : x β 0) : HasDerivAt (fun x => βx) (1 / (2 * βx)) x - Real.hasStrictDerivAt_sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{x : β} (hx : x β 0) : HasStrictDerivAt (fun x => βx) (1 / (2 * βx)) x - Differentiable.sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} (hf : Differentiable β f) (hs : β (x : E), f x β 0) : Differentiable β fun y => β(f y) - DifferentiableAt.sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {x : E} (hf : DifferentiableAt β f x) (hx : f x β 0) : DifferentiableAt β (fun y => β(f y)) x - DifferentiableWithinAt.sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {s : Set E} {x : E} (hf : DifferentiableWithinAt β f s x) (hx : f x β 0) : DifferentiableWithinAt β (fun y => β(f y)) s x - DifferentiableOn.sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {s : Set E} (hf : DifferentiableOn β f s) (hs : β x β s, f x β 0) : DifferentiableOn β (fun y => β(f y)) s - Real.deriv_sqrt_aux π Mathlib.Analysis.SpecialFunctions.Sqrt
{x : β} (hx : x β 0) : HasStrictDerivAt (fun x => βx) (1 / (2 * βx)) x β§ β (n : WithTop ββ), ContDiffAt β n (fun x => βx) x - deriv_sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{f : β β β} {x : β} (hf : DifferentiableAt β f x) (hx : f x β 0) : deriv (fun x => β(f x)) x = deriv f x / (2 * β(f x)) - derivWithin_sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{f : β β β} {s : Set β} {x : β} (hf : DifferentiableWithinAt β f s x) (hx : f x β 0) (hxs : UniqueDiffWithinAt β s x) : derivWithin (fun x => β(f x)) s x = derivWithin f s x / (2 * β(f x)) - HasDerivAt.sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{f : β β β} {f' x : β} (hf : HasDerivAt f f' x) (hx : f x β 0) : HasDerivAt (fun y => β(f y)) (f' / (2 * β(f x))) x - HasStrictDerivAt.sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{f : β β β} {f' x : β} (hf : HasStrictDerivAt f f' x) (hx : f x β 0) : HasStrictDerivAt (fun t => β(f t)) (f' / (2 * β(f x))) x - HasDerivWithinAt.sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{f : β β β} {s : Set β} {f' x : β} (hf : HasDerivWithinAt f f' s x) (hx : f x β 0) : HasDerivWithinAt (fun y => β(f y)) (f' / (2 * β(f x))) s x - HasFDerivAt.sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {x : E} {f' : StrongDual β E} (hf : HasFDerivAt f f' x) (hx : f x β 0) : HasFDerivAt (fun y => β(f y)) ((1 / (2 * β(f x))) β’ f') x - HasStrictFDerivAt.sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {x : E} {f' : StrongDual β E} (hf : HasStrictFDerivAt f f' x) (hx : f x β 0) : HasStrictFDerivAt (fun y => β(f y)) ((1 / (2 * β(f x))) β’ f') x - HasFDerivWithinAt.sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {s : Set E} {x : E} {f' : StrongDual β E} (hf : HasFDerivWithinAt f f' s x) (hx : f x β 0) : HasFDerivWithinAt (fun y => β(f y)) ((1 / (2 * β(f x))) β’ f') s x - fderiv_sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {x : E} (hf : DifferentiableAt β f x) (hx : f x β 0) : fderiv β (fun x => β(f x)) x = (1 / (2 * β(f x))) β’ fderiv β f x - fderivWithin_sqrt π Mathlib.Analysis.SpecialFunctions.Sqrt
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace β E] {f : E β β} {s : Set E} {x : E} (hf : DifferentiableWithinAt β f s x) (hx : f x β 0) (hxs : UniqueDiffWithinAt β s x) : fderivWithin β (fun x => β(f x)) s x = (1 / (2 * β(f x))) β’ fderivWithin β f s x - OpenPartialHomeomorph.univUnitBall_apply π Mathlib.Analysis.Normed.Module.Ball.Homeomorph
{E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace β E] (x : E) : βOpenPartialHomeomorph.univUnitBall x = (β(1 + βxβ ^ 2))β»ΒΉ β’ x - OpenPartialHomeomorph.univUnitBall_symm_apply π Mathlib.Analysis.Normed.Module.Ball.Homeomorph
{E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace β E] (y : E) : βOpenPartialHomeomorph.univUnitBall.symm y = (β(1 - βyβ ^ 2))β»ΒΉ β’ y - strictConcaveOn_sqrt_mul_log_Ioi π Mathlib.Analysis.Convex.SpecificFunctions.Deriv
: StrictConcaveOn β (Set.Ioi 1) fun x => βx * Real.log x - deriv_sqrt_mul_log π Mathlib.Analysis.Convex.SpecificFunctions.Deriv
(x : β) : deriv (fun x => βx * Real.log x) x = (2 + Real.log x) / (2 * βx) - deriv_sqrt_mul_log' π Mathlib.Analysis.Convex.SpecificFunctions.Deriv
: (deriv fun x => βx * Real.log x) = fun x => (2 + Real.log x) / (2 * βx) - deriv2_sqrt_mul_log π Mathlib.Analysis.Convex.SpecificFunctions.Deriv
(x : β) : deriv^[2] (fun x => βx * Real.log x) x = -Real.log x / (4 * βx ^ 3)
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using the Loogle command from the command palette. 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.You can filter for definitions vs theorems: Using
β’ (_ : Type _)finds all definitions which provide data whileβ’ (_ : Prop)finds all theorems (and definitions of proofs).
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, _ * _, _ ^ _, |- _ < _ β _
would 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. Please review the Lean FRO Terms of Use and Privacy Policy.
This is Loogle revision 9f11169 serving mathlib revision ce5dd8c