Loogle!

Result

Found 6 definitions mentioning ContinuousWithinAt and ContinuousOn.

• ContinuousOn.continuousWithinAt 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (hf : ContinuousOn f s) (hx : x ∈ s) : ContinuousWithinAt f s x
• ContinuousOn.eq_1 📋 Mathlib.Topology.ContinuousOn
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (s : Set X) : ContinuousOn f s = ∀ x ∈ s, ContinuousWithinAt f s x
• LocallyFinite.continuousOn_iUnion' 📋 Mathlib.Topology.LocallyFinite
  {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] {f : ι → Set X} {g : X → Y} (hf : LocallyFinite f) (hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x) : ContinuousOn g (⋃ i, f i)
• continuousOn_of_locally_uniform_approx_of_continuousWithinAt 📋 Mathlib.Topology.UniformSpace.UniformConvergence
  {α : Type u} {β : Type v} [UniformSpace β] {f : α → β} {s : Set α} [TopologicalSpace α] (L : ∀ x ∈ s, ∀ u ∈ uniformity β, ∃ t ∈ nhdsWithin x s, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) : ContinuousOn f s
• tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn 📋 Mathlib.MeasureTheory.Integral.PeakFunction
  {α : Type u_1} {E : Type u_2} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] {g : α → E} {x₀ : α} {s : Set α} [CompleteSpace E] [TopologicalSpace.MetrizableSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] (hs : IsCompact s) {c : α → ℝ} (hc : ContinuousOn c s) (h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀) (hnc : ∀ x ∈ s, 0 ≤ c x) (hnc₀ : 0 < c x₀) (h₀ : x₀ ∈ closure (interior s)) (hmg : MeasureTheory.IntegrableOn g s μ) (hcg : ContinuousWithinAt g s x₀) : Filter.Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) Filter.atTop (nhds (g x₀))
• tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos 📋 Mathlib.MeasureTheory.Integral.PeakFunction
  {α : Type u_1} {E : Type u_2} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] {g : α → E} {x₀ : α} {s : Set α} [CompleteSpace E] [TopologicalSpace.MetrizableSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] (hs : IsCompact s) (hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)) {c : α → ℝ} (hc : ContinuousOn c s) (h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀) (hnc : ∀ x ∈ s, 0 ≤ c x) (hnc₀ : 0 < c x₀) (h₀ : x₀ ∈ s) (hmg : MeasureTheory.IntegrableOn g s μ) (hcg : ContinuousWithinAt g s x₀) : Filter.Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) Filter.atTop (nhds (g x₀))

About

Loogle searches Lean and Mathlib definitions and theorems.

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

Usage

Loogle finds definitions and lemmas in various ways:

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, _ * _, _ ^ _, |- _ < _ → _
woould find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 4e1aab0 serving mathlib revision 2d53f5f