Loogle!

Result

Found 12 declarations 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.UniformApproximation
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] {f : α → β} {s : Set α} (L : ∀ x ∈ s, ∀ u ∈ uniformity β, ∃ t ∈ nhdsWithin x s, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) : ContinuousOn f s
• continuousWithinAt_cfc_fun 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
  {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R A p] [TopologicalSpace X] {f : X → R → R} {a : A} {x₀ : X} {s : Set X} (h_tendsto : TendstoUniformlyOn f (f x₀) (nhdsWithin x₀ s) (spectrum R a)) (hf : ∀ᶠ (x : X) in nhdsWithin x₀ s, ContinuousOn (f x) (spectrum R a)) : ContinuousWithinAt (fun x => cfc (f x) a) s x₀
• ContinuousWithinAt.cfc_nnreal 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
  {X : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [TopologicalSpace X] {s : Set NNReal} (hs : IsCompact s) (f : NNReal → NNReal) {a : X → A} {x₀ : X} {t : Set X} (hx₀ : x₀ ∈ t) (ha_cont : ContinuousWithinAt a t x₀) (ha : ∀ᶠ (x : X) in nhdsWithin x₀ t, spectrum NNReal (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in nhdsWithin x₀ t, 0 ≤ a x) (hf : ContinuousOn f s := by cfc_cont_tac) : ContinuousWithinAt (fun x => cfc f (a x)) t x₀
• continuousWithinAt_cfcₙ_fun 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
  {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [Nontrivial R] [IsTopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalContinuousFunctionalCalculus R A p] [TopologicalSpace X] {f : X → R → R} {a : A} {x₀ : X} {s : Set X} (h_tendsto : TendstoUniformlyOn f (f x₀) (nhdsWithin x₀ s) (quasispectrum R a)) (hf : ∀ᶠ (x : X) in nhdsWithin x₀ s, ContinuousOn (f x) (quasispectrum R a)) (hf0 : ∀ᶠ (x : X) in nhdsWithin x₀ s, f x 0 = 0 := by cfc_zero_tac) : ContinuousWithinAt (fun x => cfcₙ (f x) a) s x₀
• ContinuousWithinAt.cfc 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
  {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜) {a : X → A} {x₀ : X} {t : Set X} (hx₀ : x₀ ∈ t) (ha_cont : ContinuousWithinAt a t x₀) (ha : ∀ᶠ (x : X) in nhdsWithin x₀ t, spectrum 𝕜 (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in nhdsWithin x₀ t, p (a x)) (hf : ContinuousOn f s := by cfc_cont_tac) : ContinuousWithinAt (fun x => cfc f (a x)) t x₀
• ContinuousWithinAt.cfcₙ_nnreal 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
  {X : Type u_1} {A : Type u_2} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [TopologicalSpace X] {s : Set NNReal} (hs : IsCompact s) (f : NNReal → NNReal) {a : X → A} {x₀ : X} {t : Set X} (hx₀ : x₀ ∈ t) (ha_cont : ContinuousWithinAt a t x₀) (ha : ∀ᶠ (x : X) in nhdsWithin x₀ t, quasispectrum NNReal (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in nhdsWithin x₀ t, 0 ≤ a x) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : ContinuousWithinAt (fun x => cfcₙ f (a x)) t x₀
• ContinuousWithinAt.cfcₙ 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
  {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜) {a : X → A} {x₀ : X} {t : Set X} (hx₀ : x₀ ∈ t) (ha_cont : ContinuousWithinAt a t x₀) (ha : ∀ᶠ (x : X) in nhdsWithin x₀ t, quasispectrum 𝕜 (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in nhdsWithin x₀ t, p (a x)) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : ContinuousWithinAt (fun x => cfcₙ f (a x)) t x₀
• 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, _ * _, _ ^ _, |- _ < _ → _
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 3e2b26a