ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 (s.indicator 1 x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>this : IsLocallyFiniteMeasure (μ.restrict s)<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 (s.indicator 1 x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>this : IsLocallyFiniteMeasure (μ.restrict s)<GOAL>∀ (a : α), Tendsto (fun a => (μ.restrict s) a / μ a) (v.filterAt a) (𝓝 ((μ.restrict s).rnDeriv μ a)) → (μ.restrict s).rnDeriv μ a = s.indicator 1 a → Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt a) (𝓝 (s.indicator 1 a))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>this : IsLocallyFiniteMeasure (μ.restrict s)<VAR>x : α<VAR>hx : Tendsto (fun a => (μ.restrict s) a / μ a) (v.filterAt x) (𝓝 ((μ.restrict s).rnDeriv μ x))<VAR>h'x : (μ.restrict s).rnDeriv μ x = s.indicator 1 x<GOAL>Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 (s.indicator 1 x))
<VAR>a x✝ z x : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(↑r * x).arg = x.arg
<VAR>a x z : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(↑r * 0).arg = arg 0
<VAR>a x✝ z x : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hx : x ≠ 0<GOAL>(↑r * x).arg = x.arg
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>n✝ : ℕ<VAR>f : Fin (n✝ + 1) → α<VAR>a : α<VAR>n : ℕ<VAR>x : { x // x ≠ last n }<GOAL>(finSuccAboveOrderIso (last n)).symm x = (↑x).castLT ⋯
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>n✝ : ℕ<VAR>f : Fin (n✝ + 1) → α<VAR>a : α<VAR>n : ℕ<VAR>x : { x // x ≠ last n }<GOAL>some ((finSuccAboveOrderIso (last n)).symm x) = some ((↑x).castLT ⋯)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s t : Set α<VAR>h : Disjoint s t<GOAL>supported M R s ⊓ supported M R t = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K✝ : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>n : ℕ<VAR>h_dim : finrank 𝕜 ↥K + n = finrank 𝕜 E<GOAL>finrank 𝕜 ↥Kᗮ = n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K✝ : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>n : ℕ<VAR>h_dim : finrank 𝕜 ↥K + n = finrank 𝕜 E<GOAL>finrank 𝕜 ↥K + finrank 𝕜 ↥Kᗮ = finrank 𝕜 ↥K + n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure α<VAR>ν : Measure β<VAR>e : α ≃ᵐ β<VAR>μ₁ μ₂ : Measure α<VAR>hμ : Measure.map (⇑e.symm) (Measure.map (⇑e) μ₁) = Measure.map (⇑e.symm) (Measure.map (⇑e) μ₂)<GOAL>μ₁ = μ₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedAddCommGroup E<VAR>inst✝⁴ : SeminormedAddCommGroup F<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : NormedSpace 𝕜 G<VAR>x✝ : E × F<VAR>e : E<VAR>f : F<GOAL>‖(snd 𝕜 E F) (e, f)‖ ≤ 1 * ‖(e, f)‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>inst✝ : PathConnectedSpace X<VAR>f : X → Y<VAR>hf : Surjective f<VAR>hf' : Continuous f<GOAL>PathConnectedSpace Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>inst✝ : PathConnectedSpace X<VAR>f : X → Y<VAR>hf : Surjective f<VAR>hf' : Continuous f<GOAL>IsPathConnected (range f)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>m ≤ n.succ ↔ m ≤ n ∨ m = n.succ
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>m ≤ n ∨ m = n.succ → m ≤ n.succ
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x x' z : H<VAR>v : E<GOAL>((tangentBundleCore I H).coordChange (achart H x) (achart H x') z) v = (ContinuousLinearMap.id 𝕜 E) v
<VAR>α : Type w<VAR>inst✝ : Finite α<VAR>X : α → Profinite<VAR>B : Profinite<VAR>π : (a : α) → X a ⟶ B<VAR>a : α<VAR>x : (forget Profinite).obj (X a)<GOAL>(ι X a ≫ desc X π) x = (π a) x
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha : a ≠ 0<GOAL>b.factorization ≤ (a * b).factorization
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha : a ≠ 0<GOAL>b.factorization ≤ (b * a).factorization
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>hf : Measurable f<GOAL>∫⁻ (x : β), f x ∂(deterministic g hg) a = f (g a)
<VAR>z : ℂ<VAR>n : ℕ<GOAL>(z / ↑n).im = z.im / ↑n
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : 0 ∉ t<VAR>a✝ : Nontrivial R<GOAL>t.prod.natDegree = (Multiset.map natDegree t).sum
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : 0 ∉ t<VAR>a✝ : Nontrivial R<GOAL>(Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : 0 ∉ t<VAR>a✝ : Nontrivial R<GOAL>¬∃ a ∈ t, a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>a b : α<GOAL>toLowerSet a ⤳ toLowerSet b ↔ a ≤ b
<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>z : ℍ<VAR>hk' : 2 < ↑k<GOAL>Summable fun x => ‖eisSummand k x z‖
<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>z : ℍ<VAR>hk' : 2 < ↑k<GOAL>∀ (b : Fin 2 → ℤ), Complex.abs (eisSummand k b z) ≤ r z ^ (-↑k) * ‖b‖ ^ (-↑k)
<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>z : ℍ<VAR>hk' : 2 < ↑k<VAR>b : Fin 2 → ℤ<GOAL>Complex.abs (eisSummand k b z) ≤ r z ^ (-↑k) * ‖b‖ ^ (-↑k)
<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>z : ℍ<VAR>hk' : 2 < ↑k<VAR>b : Fin 2 → ℤ<GOAL>Complex.abs (↑(b 0) * ↑z + ↑(b 1)) ^ (-k) ≤ r z ^ (-↑k) * ‖b‖ ^ (-↑k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝ : Zero β<VAR>f : α →ₛ β<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>↑(f.restrict s) = s.indicator ↑f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r : R[X]<VAR>M : R[X] → Prop<VAR>p : R[X]<VAR>h_add : ∀ (p q : R[X]), M p → M q → M (p + q)<VAR>h_monomial : ∀ (n : ℕ) (a : R), M ((monomial n) a)<VAR>n : ℕ<VAR>a : R<VAR>_h : M (C a * X ^ n)<GOAL>M (C a * X ^ (n + 1))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r : R[X]<VAR>M : R[X] → Prop<VAR>p : R[X]<VAR>h_add : ∀ (p q : R[X]), M p → M q → M (p + q)<VAR>h_monomial : ∀ (n : ℕ) (a : R), M ((monomial n) a)<VAR>n : ℕ<VAR>a : R<VAR>_h : M (C a * X ^ n)<GOAL>M ((monomial (n + 1)) a)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>h✝ h : α ≃ᵢ β<VAR>x : β<VAR>r : ℝ<GOAL>⇑h ⁻¹' Metric.sphere x r = Metric.sphere (h.symm x) r
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>I : MulticospanIndex C<VAR>inst✝¹ : HasMultiequalizer I<VAR>inst✝ : PreservesLimit I.multicospan (forget C)<VAR>x y : (forget C).obj (multiequalizer I)<VAR>h : ∀ (t : I.L), (Multiequalizer.ι I t) x = (Multiequalizer.ι I t) y<GOAL>x = y
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>I : MulticospanIndex C<VAR>inst✝¹ : HasMultiequalizer I<VAR>inst✝ : PreservesLimit I.multicospan (forget C)<VAR>x y : (forget C).obj (multiequalizer I)<VAR>h : ∀ (t : I.L), (Multiequalizer.ι I t) x = (Multiequalizer.ι I t) y<GOAL>∀ (j : WalkingMulticospan I.fstTo I.sndTo), (limit.π I.multicospan j) x = (limit.π I.multicospan j) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : Ordinal.{u} → Ordinal.{max u v}<VAR>H : IsNormal f<VAR>o : Ordinal.{u}<VAR>h : o.IsLimit<GOAL>(o.bsup fun x x_1 => f x) = f o
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : BarrelledSpace 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : ∀ (i : ι), Continuous ⇑(p i)<VAR>bdd : BddAbove (range p)<GOAL>Continuous (⨆ i, ⇑(p i))
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : BarrelledSpace 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : ∀ (i : ι), Continuous ⇑(p i)<VAR>bdd : BddAbove (range p)<GOAL>Continuous ⇑(⨆ i, p i)
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : BarrelledSpace 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : ∀ (i : ι), Continuous ⇑(p i)<VAR>bdd : BddAbove (range p)<GOAL>LowerSemicontinuous ⇑(⨆ i, p i)
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : BarrelledSpace 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : ∀ (i : ι), Continuous ⇑(p i)<VAR>bdd : BddAbove (range p)<GOAL>LowerSemicontinuous (⨆ i, ⇑(p i))
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : BarrelledSpace 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : ∀ (i : ι), Continuous ⇑(p i)<VAR>bdd : ∀ (x : E), BddAbove (range fun i => (p i) x)<GOAL>LowerSemicontinuous (⨆ i, ⇑(p i))
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : BarrelledSpace 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : ∀ (i : ι), Continuous ⇑(p i)<VAR>bdd : ∀ (x : E), BddAbove (range fun i => (p i) x)<VAR>x✝ : E<GOAL>(⨆ i, ⇑(p i)) x✝ = ⨆ i, (p i) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g✝ g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>hf : SurjOn f s t<VAR>g : β → γ<GOAL>SurjOn (g ∘ f) s (g '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g✝ g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>hf : SurjOn f s t<VAR>g : β → γ<GOAL>g '' t ⊆ g '' (f '' s)
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s s₁ s₂ : Set α<VAR>h : m.IsCaratheodory sᶜ<GOAL>m.IsCaratheodory s
<VAR>G : Type u_1<VAR>inst✝³ : MeasurableSpace G<VAR>μ : Measure G<VAR>g✝ : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → ℝ≥0∞<VAR>g : G<GOAL>∫⁻ (x : G), f (x * g) ∂μ = ∫⁻ (x : G), f x ∂μ
<VAR>G : Type u_1<VAR>inst✝³ : MeasurableSpace G<VAR>μ : Measure G<VAR>g✝ : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → ℝ≥0∞<VAR>g : G<GOAL>∫⁻ (x : G), f x ∂μ = ∫⁻ (a : G), f a ∂map (⇑(MeasurableEquiv.mulRight g)) μ
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>x : ↑(inducedMap A).fst<VAR>n : ℕ<GOAL>(inducedMap A).snd x ∈ A (res (↑x) n)
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>x : ↑(inducedMap A).fst<VAR>n : ℕ<VAR>this : Set.Nonempty.some ⋯ ∈ ⋂ n, A (res (↑x) n)<GOAL>(inducedMap A).snd x ∈ A (res (↑x) n)
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>x : ↑(inducedMap A).fst<VAR>n : ℕ<VAR>this : ∀ (i : ℕ), Set.Nonempty.some ⋯ ∈ A (res (↑x) i)<GOAL>(inducedMap A).snd x ∈ A (res (↑x) n)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<GOAL>∀ᶠ (y : E) in 𝓝 0, HasSum (fun n => (p n) fun x => y) (f (x + y))
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>V W : Set (β × β)<VAR>x y z : β<VAR>hV : SymmetricRel V<VAR>hx : x ∈ ball z V<VAR>hy : y ∈ ball z W<GOAL>(x, y) ∈ V ○ W
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>V W : Set (β × β)<VAR>x y z : β<VAR>hV : SymmetricRel V<VAR>hx : z ∈ ball x V<VAR>hy : y ∈ ball z W<GOAL>(x, y) ∈ V ○ W
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>x y : E<VAR>r✝ : ℝ<VAR>p q : Seminorm 𝕜 E<VAR>e : E<VAR>r : ℝ<GOAL>(p ⊔ q).closedBall e r = p.closedBall e r ∩ q.closedBall e r
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<GOAL>↑(λ ^ 2) = ↑(-3 * ↑η)
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>h : s =ᶠ[𝓝 x] t<GOAL>derivWithin f s x = derivWithin f t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>π : δ → Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : (a : δ) → MeasurableSpace (π a)<VAR>inst✝ : MeasurableSpace γ<VAR>s : Set δ<VAR>t : (i : δ) → Set (π i)<VAR>hs : s.Countable<GOAL>MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>π : δ → Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : (a : δ) → MeasurableSpace (π a)<VAR>inst✝ : MeasurableSpace γ<VAR>s : Set δ<VAR>t : (i : δ) → Set (π i)<VAR>hs : s.Countable<VAR>h : s.pi t = ∅<GOAL>MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>π : δ → Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : (a : δ) → MeasurableSpace (π a)<VAR>inst✝ : MeasurableSpace γ<VAR>s : Set δ<VAR>t : (i : δ) → Set (π i)<VAR>hs : s.Countable<VAR>h : (s.pi t).Nonempty<GOAL>MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ t s : Set α<VAR>hs : IsSeparable s<GOAL>SeparableSpace ↑s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ t✝ s : Set α<VAR>hs : IsSeparable s<VAR>t : Set α<VAR>hts : t ⊆ s<VAR>htc : t.Countable<VAR>hst : s ⊆ closure t<GOAL>SeparableSpace ↑s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ t✝ s : Set α<VAR>hs : IsSeparable s<VAR>t : Set ↑s<VAR>htc : (Subtype.val '' t).Countable<VAR>hst : s ⊆ closure (Subtype.val '' t)<GOAL>SeparableSpace ↑s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ t✝ s : Set α<VAR>hs : IsSeparable s<VAR>t : Set ↑s<VAR>htc : (Subtype.val '' t).Countable<VAR>hst : s ⊆ closure (Subtype.val '' t)<GOAL>Dense t
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<GOAL>(fun t => inverse (↑x + t)) =O[𝓝 0] fun _t => 1
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<GOAL>(fun x_1 => inverse (1 + ↑x⁻¹ * x_1) * ↑x⁻¹) =O[𝓝 0] fun _t => 1 * 1
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<GOAL>(fun x_1 => inverse (1 - -↑x⁻¹ * x_1) * ↑x⁻¹) =O[𝓝 0] fun _t => 1 * 1
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)<GOAL>(fun x_1 => inverse (1 - -↑x⁻¹ * x_1) * ↑x⁻¹) =O[𝓝 0] fun _t => 1 * 1
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<GOAL>ContMDiffWithinAt I I' n f (insert x s) x ↔ ContMDiffWithinAt I I' n f s x
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<GOAL>ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' insert x s ∩ range ↑I) (↑(extChartAt I x) x) ↔ ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)