ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>x✝ : 𝕜<GOAL>(fderivWithin 𝕜 f univ x✝) 1 = (fderiv 𝕜 f x✝) 1
<VAR>R : Type u_1<VAR>S : Type ?u.132402<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.132867<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.134007<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : Module.Finite R M<VAR>ι : Type u_3<VAR>f : ι → M<VAR>b : Basis ι k (k ⊗[R] M)<VAR>hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i<GOAL>Submodule.span R (Set.range f) = ⊤
<VAR>R : Type u_1<VAR>S : Type ?u.132402<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.132867<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.134007<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : Module.Finite R M<VAR>ι : Type u_3<VAR>f : ι → M<VAR>b : Basis ι k (k ⊗[R] M)<VAR>hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i<GOAL>Submodule.span k (Set.range (⇑((mk R k M) 1) ∘ f)) = Submodule.span k (Set.range ⇑b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j : JordanDecomposition α<VAR>r : ℝ≥0<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(r • j).toSignedMeasure i = ↑(r • j.toSignedMeasure) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0<GOAL>∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0<VAR>g : α → ℝ≥0∞<VAR>hgf : g ≤ f<VAR>hg_meas : Measurable g<VAR>hgsupp : μ (support g) < ⊤<VAR>hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ<GOAL>∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0<VAR>g : α → ℝ≥0∞<VAR>hgf : g ≤ f<VAR>hg_meas : Measurable g<VAR>hgsupp : μ (support g) < ⊤<VAR>hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ<GOAL>∫⁻ (a : α) in (support g)ᶜ, f a ∂μ < ε
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝.Hom Y✝<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsOpenImmersion f<VAR>U : Y.Opens<VAR>V : X.Opens<VAR>e : V ≤ f ⁻¹ᵁ U<GOAL>appLE f U V e ≫ (appIso f V).inv = Y.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝.Hom Y✝<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsOpenImmersion f<VAR>U : Y.Opens<VAR>V : X.Opens<VAR>e : V ≤ f ⁻¹ᵁ U<GOAL>Y.presheaf.map (homOfLE ⋯).op ≫ Y.presheaf.map (homOfLE ⋯).op = Y.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝.Hom Y✝<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsOpenImmersion f<VAR>U : Y.Opens<VAR>V : X.Opens<VAR>e : V ≤ f ⁻¹ᵁ U<GOAL>Y.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) = Y.presheaf.map (homOfLE ⋯).op
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<GOAL>(η.withDensity (κ.rnDeriv η)) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>h_eq_add : η.withDensity (κ.rnDeriv η) + κ.singularPart η = κ<GOAL>(η.withDensity (κ.rnDeriv η)) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>h_eq_add : ∀ (a : α) (s : Set γ), MeasurableSet s → ((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a) s = (κ a) s<GOAL>(η.withDensity (κ.rnDeriv η)) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>h_eq_add : ((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a) (κ.mutuallySingularSetSlice η a)ᶜ = (κ a) (κ.mutuallySingularSetSlice η a)ᶜ<GOAL>(η.withDensity (κ.rnDeriv η)) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>h_eq_add : ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = (κ a) (κ.mutuallySingularSetSlice η a)ᶜ<GOAL>(η.withDensity (κ.rnDeriv η)) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>h_eq_add : ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = (κ a) (κ.mutuallySingularSetSlice η a)ᶜ<GOAL>(η.withDensity (κ.rnDeriv η)) a = 0 ↔ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p₁ p₂ : P<VAR>v : V<GOAL>v +ᵥ p₁ ∈ affineSpan k {p₁, p₂} ↔ ∃ r, r • (p₂ -ᵥ p₁) = v
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g volume t₁ t₂<VAR>hT : 0 < T<VAR>t : ℝ<VAR>ε : ℝ := Int.fract (t / T) * T<GOAL>∫ (x : ℝ) in 0 ..t, g x ≤ sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g volume t₁ t₂<VAR>hT : 0 < T<VAR>t : ℝ<VAR>ε : ℝ := Int.fract (t / T) * T<GOAL>(∫ (x : ℝ) in 0 ..ε, g x) + ∫ (x : ℝ) in ε..Int.fract (t / T) * T + ⌊t / T⌋ • T, g x ≤ sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g volume t₁ t₂<VAR>hT : 0 < T<VAR>t : ℝ<VAR>ε : ℝ := Int.fract (t / T) * T<GOAL>∫ (x : ℝ) in 0 ..ε, g x ≤ sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>β : Type u_3<VAR>f : ι → α → β<VAR>t : ι → Set β<VAR>ht : IndexedPartition t<VAR>hf : ∀ (i : ι), BijOn (f i) (s i) (t i)<VAR>g : α → β := hs.piecewise f<VAR>hg : g = hs.piecewise f<GOAL>Bijective g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>β : Type u_3<VAR>f : ι → α → β<VAR>t : ι → Set β<VAR>ht : IndexedPartition t<VAR>hf : ∀ (i : ι), BijOn (f i) (s i) (t i)<VAR>g : α → β := hs.piecewise f<VAR>hg : g = hs.piecewise f<VAR>hg_bij : ∀ (i : ι), BijOn g (s i) (t i)<GOAL>Bijective g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>β : Type u_3<VAR>f : ι → α → β<VAR>t : ι → Set β<VAR>ht : IndexedPartition t<VAR>hf : ∀ (i : ι), BijOn (f i) (s i) (t i)<VAR>g : α → β := hs.piecewise f<VAR>hg : g = hs.piecewise f<VAR>hg_bij : ∀ (i : ι), BijOn g (s i) (t i)<VAR>hg_inj : InjOn g (⋃ i, s i)<GOAL>Bijective g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>β : Type u_3<VAR>f : ι → α → β<VAR>t : ι → Set β<VAR>ht : IndexedPartition t<VAR>hf : ∀ (i : ι), BijOn (f i) (s i) (t i)<VAR>g : α → β := hs.piecewise f<VAR>hg : g = hs.piecewise f<VAR>hg_bij : ∀ (i : ι), BijOn g (s i) (t i)<VAR>hg_inj : InjOn g (⋃ i, s i)<GOAL>BijOn g (⋃ i, s i) (⋃ i, t i)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : IsFreeGroup G<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>f : Generators G → H<GOAL>∃! F, ∀ (a : Generators G), F (of a) = f a
<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>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Algebra R 𝕜<VAR>p : 𝕜[X]<VAR>q : R[X]<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun x => (aeval x) q) s x = (aeval x) (derivative q)
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>a b : Complementeds α<GOAL>IsCompl ↑a ↑b ↔ IsCompl a b
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<GOAL>∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • t)).Nonempty
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>t' : Set E<VAR>t'_meas : MeasurableSet t'<VAR>t't : t' ⊆ t<VAR>t'pos : 0 < μ t'<VAR>t'top : μ t' < ⊤<GOAL>∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • t)).Nonempty
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>t' : Set E<VAR>t'_meas : MeasurableSet t'<VAR>t't : t' ⊆ t<VAR>t'pos : 0 < μ t'<VAR>t'top : μ t' < ⊤<GOAL>∀ (a : ℝ), 0 < μ (s ∩ ({x} + a • t')) / μ ({x} + a • t') → (s ∩ ({x} + a • t)).Nonempty
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>t' : Set E<VAR>t'_meas : MeasurableSet t'<VAR>t't : t' ⊆ t<VAR>t'pos : 0 < μ t'<VAR>t'top : μ t' < ⊤<VAR>r : ℝ<VAR>hr : 0 < μ (s ∩ ({x} + r • t')) / μ ({x} + r • t')<GOAL>(s ∩ ({x} + r • t)).Nonempty
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>t' : Set E<VAR>t'_meas : MeasurableSet t'<VAR>t't : t' ⊆ t<VAR>t'pos : 0 < μ t'<VAR>t'top : μ t' < ⊤<VAR>r : ℝ<VAR>hr : 0 < μ (s ∩ ({x} + r • t')) / μ ({x} + r • t')<VAR>this : μ (s ∩ ({x} + r • t')) ≠ 0<GOAL>(s ∩ ({x} + r • t)).Nonempty
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>t' : Set E<VAR>t'_meas : MeasurableSet t'<VAR>t't : t' ⊆ t<VAR>t'pos : 0 < μ t'<VAR>t'top : μ t' < ⊤<VAR>r : ℝ<VAR>hr : 0 < μ (s ∩ ({x} + r • t')) / μ ({x} + r • t')<VAR>this✝ : μ (s ∩ ({x} + r • t')) ≠ 0<VAR>this : (s ∩ ({x} + r • t')).Nonempty<GOAL>(s ∩ ({x} + r • t)).Nonempty
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>t' : Set E<VAR>t'_meas : MeasurableSet t'<VAR>t't : t' ⊆ t<VAR>t'pos : 0 < μ t'<VAR>t'top : μ t' < ⊤<VAR>r : ℝ<VAR>hr : 0 < μ (s ∩ ({x} + r • t')) / μ ({x} + r • t')<VAR>this✝ : μ (s ∩ ({x} + r • t')) ≠ 0<VAR>this : (s ∩ ({x} + r • t')).Nonempty<GOAL>{x} + r • t' ⊆ {x} + r • t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>s : Multiset γ<VAR>f : γ → α<GOAL>∀ (a : γ) (s : Multiset γ), (∀ {t : Multiset β}, Rel r (map f s) t ↔ Rel (fun a b => r (f a) b) s t) → ∀ {t : Multiset β}, Rel r (map f (a ::ₘ s)) t ↔ Rel (fun a b => r (f a) b) (a ::ₘ s) t
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S x<GOAL>f' < slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S x<GOAL>S ∈ 𝓝[>] x
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S x<GOAL>∃ u ∈ Ioi x, Ioc x u ⊆ S
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>v : V<VAR>hv : v ∈ s.direction<GOAL>s.WSameSide x (v +ᵥ y) ↔ s.WSameSide x y
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hf : HasFDerivAtFilter f f' x L<VAR>hg : HasFDerivAtFilter g g' x L<GOAL>HasFDerivAtFilter (fun x => f x - g x) (f' - g') x L
<VAR>T : ℝ<VAR>m n : ℤ<VAR>x : AddCircle T<GOAL>↑((m + n) • x).toCircle = (fourier m) x * (fourier n) x
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>X Y : C<VAR>inst✝¹ : HasBinaryBiproduct X Y<VAR>inst✝ : PreservesBinaryBiproduct X Y F<VAR>W : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<GOAL>F.map (lift f g) ≫ (F.mapBiprod X Y).hom = lift (F.map f) (F.map g)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : C<VAR>Y : Over X<VAR>Z : C<VAR>g : Z ⟶ Y.left<GOAL>((overEquiv Y) ⊤).arrows g ↔ ⊤.arrows g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : C<VAR>Y : Over X<VAR>Z : C<VAR>g : Z ⟶ Y.left<GOAL>((overEquiv Y) ⊤).arrows g
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z p₁ p₂ : P<GOAL>midpoint R p₁ p₂ -ᵥ p₂ = ⅟2 • (p₁ -ᵥ p₂)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p : R⟦X⟧<VAR>n d : ℕ<GOAL>(coeff R (d + n)) (p * X ^ n) = (coeff R d) p
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p : R⟦X⟧<VAR>n d : ℕ<GOAL>∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → (coeff R b.1) p * (coeff R b.2) (X ^ n) = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p : R⟦X⟧<VAR>n d : ℕ<GOAL>(d, n) ∉ antidiagonal (d + n) → (coeff R (d, n).1) p * (coeff R (d, n).2) (X ^ n) = 0
<VAR>V : Type u<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace ℝ V<VAR>inst✝ : CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<GOAL>ker (continuousLinearMapOfBilin B) = ⊥
<VAR>V : Type u<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace ℝ V<VAR>inst✝ : CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<GOAL>Function.Injective ⇑(continuousLinearMapOfBilin B)
<VAR>V : Type u<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace ℝ V<VAR>inst✝ : CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<VAR>w✝ : ℝ≥0<VAR>left✝ : 0 < w✝<VAR>antilipschitz : AntilipschitzWith w✝ ⇑(continuousLinearMapOfBilin B)<GOAL>Function.Injective ⇑(continuousLinearMapOfBilin B)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y✝ x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>s t s' t' : R<VAR>h' : s • x + t • y = s' • x + t' • y<GOAL>s = s' ∧ t = t'
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y✝ x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>s t s' t' : R<VAR>h' : s • x + t • y = s' • x + t' • y<VAR>this : (s - s') • x + (t - t') • y = 0<GOAL>s = s' ∧ t = t'
<VAR>x : PGame<VAR>h : x ⧏ 0<GOAL>x⁻¹ = -(-x).inv'
<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>n✝ m : ℕ<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>k : ℕ<VAR>hk : n ≤ k<GOAL>p.changeOrigin x k = 0
<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>n✝ m : ℕ<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>k : ℕ<VAR>hk : n ≤ k<GOAL>(p.changeOriginSeries k).partialSum (n - k) x = 0
<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>n✝ m : ℕ<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>k : ℕ<VAR>hk : n ≤ k<GOAL>∀ x_1 ∈ Finset.range (n - k), ((p.changeOriginSeries k x_1) fun x_2 => x) = 0
<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>n✝ m✝ : ℕ<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>k : ℕ<VAR>hk : n ≤ k<VAR>m : ℕ<VAR>hm : m ∈ Finset.range (n - k)<GOAL>((p.changeOriginSeries k m) fun x_1 => x) = 0
<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>n✝ m✝ : ℕ<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>k : ℕ<VAR>hk : n ≤ k<VAR>m : ℕ<VAR>hm : m < n - k<GOAL>((p.changeOriginSeries k m) fun x_1 => x) = 0
<VAR>ι : Type u_1<VAR>𝕜✝ : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f✝ g : ℝ → E<VAR>μ : Measure ℝ<VAR>𝕜 : Type u_6<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : ℝ → 𝕜<VAR>c : E<GOAL>∫ (x : ℝ) in a..b, f x • c ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) • c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b