Loogle!

Result

Found 7 declarations mentioning Norm.norm, Real, Real.instLT, Real.instOne, Filter.Tendsto, LT.lt, One.toOfNat1 and OfNat.ofNat. Of these, 5 match your pattern(s).

• tendsto_pow_atTop_nhds_zero_of_norm_lt_one 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_2} [SeminormedRing R] {x : R} (h : ‖x‖ < 1) : Filter.Tendsto (fun n => x ^ n) Filter.atTop (nhds 0)
• tendsto_pow_atTop_nhds_zero_iff_norm_lt_one 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_2} [SeminormedRing R] [NormMulClass R] {x : R} : Filter.Tendsto (fun n => x ^ n) Filter.atTop (nhds 0) ↔ ‖x‖ < 1
• CStarAlgebra.tendsto_mul_right_of_forall_nonneg_tendsto 📋 Mathlib.Analysis.CStarAlgebra.ApproximateUnit
  {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {l : Filter A} (h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Filter.Tendsto (fun x => x * m) l (nhds m)) (m : A) : Filter.Tendsto (fun x => x * m) l (nhds m)
• Complex.abel_aux 📋 Mathlib.Analysis.Complex.AbelLimit
  {f : ℕ → ℂ} {l : ℂ} (h : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l)) {z : ℂ} (hz : ‖z‖ < 1) : Filter.Tendsto (fun n => (1 - z) * ∑ i ∈ Finset.range n, (l - ∑ j ∈ Finset.range (i + 1), f j) * z ^ i) Filter.atTop (nhds (l - ∑' (n : ℕ), f n * z ^ n))
• PadicInt.continuousAddCharEquiv_of_norm_mul_symm_apply 📋 Mathlib.NumberTheory.Padics.AddChar
  {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] [NormMulClass R] {r : R} (hr : ‖r‖ < 1) : ↑((PadicInt.continuousAddCharEquiv_of_norm_mul p R).symm ⟨r, hr⟩) = PadicInt.addChar_of_value_at_one r ⋯

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

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

4. 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 find tsum_lt_tsum even though the hypothesis f 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, _ * _, _ ^ _, |- _ < _ → _
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.

This is Loogle revision 19971e9 serving mathlib revision bce1d65