ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.IsIdempotentComplete C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>(CategoryTheory.Idempotents.DoldKan.isoN₁.hom.app X).f = AlgebraicTopology.DoldKan.PInfty
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.IsIdempotentComplete C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<GOAL>(AlgebraicTopology.DoldKan.N₂.map (CategoryTheory.Idempotents.DoldKan.isoΓ₀.hom.app X)).f = AlgebraicTopology.DoldKan.PInfty
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.IsIdempotentComplete C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>CategoryTheory.Idempotents.DoldKan.equivalence.functor = CategoryTheory.Idempotents.DoldKan.N
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.IsIdempotentComplete C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>CategoryTheory.Idempotents.DoldKan.equivalence.inverse = CategoryTheory.Idempotents.DoldKan.Γ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.IsIdempotentComplete C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>AlgebraicTopology.DoldKan.Compatibility.τ₀ = AlgebraicTopology.DoldKan.Compatibility.τ₁ CategoryTheory.Idempotents.DoldKan.isoN₁ CategoryTheory.Idempotents.DoldKan.isoΓ₀ AlgebraicTopology.DoldKan.N₁Γ₀
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.IsIdempotentComplete C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>i : ℕ<GOAL>(CategoryTheory.Idempotents.DoldKan.η.inv.app X).f i = ((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).unitIso.hom.app X).f i ≫ ((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.map (AlgebraicTopology.DoldKan.N₁Γ₀.inv.app X)).f i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.IsIdempotentComplete C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>i : ℕ<GOAL>(CategoryTheory.Idempotents.DoldKan.η.hom.app X).f i = ((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.map (AlgebraicTopology.DoldKan.N₁Γ₀.hom.app X)).f i ≫ ((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).unitIso.inv.app X).f i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.IsIdempotentComplete C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>CategoryTheory.Idempotents.DoldKan.equivalence.counitIso = CategoryTheory.Idempotents.DoldKan.η
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.IsIdempotentComplete C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>AlgebraicTopology.DoldKan.Compatibility.υ CategoryTheory.Idempotents.DoldKan.isoN₁ = AlgebraicTopology.DoldKan.Γ₂N₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.IsIdempotentComplete C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>CategoryTheory.Idempotents.DoldKan.equivalence.unitIso = CategoryTheory.Idempotents.DoldKan.ε
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : SimplexCategoryᵒᵖ} (f : X ⟶ Y) (x : CategoryTheory.ComposableArrows C (Opposite.unop X).len), (CategoryTheory.nerve C).map f x = x.whiskerLeft (SimplexCategory.toCat.map f.unop)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Δ : SimplexCategoryᵒᵖ<GOAL>(CategoryTheory.nerve C).obj Δ = CategoryTheory.ComposableArrows C (Opposite.unop Δ).len
<GOAL>∀ {X Y : CategoryTheory.Cat} (F : X ⟶ Y) (Δ : SimplexCategoryᵒᵖ) (a : CategoryTheory.ComposableArrows (↑X) (Opposite.unop Δ).len), (CategoryTheory.nerveFunctor.map F).app Δ a = (CategoryTheory.Functor.mapComposableArrows F (Opposite.unop Δ).len).obj a
<VAR>C : CategoryTheory.Cat<GOAL>CategoryTheory.nerveFunctor.obj C = CategoryTheory.nerve ↑C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>x : CategoryTheory.nerve C _[n + 1]<GOAL>CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) 0 x = CategoryTheory.ComposableArrows.δ₀ x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>SecondCountableTopologyEither (E →L[𝕜] F) E<VAR>MeasurableSpace F<VAR>BorelSpace F<GOAL>Measurable fun p => p.1 p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>L : E →L[𝕜] F<VAR>r ε : ℝ<GOAL>IsOpen (FDerivMeasurableAux.A f L r ε)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s ε : ℝ<GOAL>IsOpen (FDerivMeasurableAux.B f K r s ε)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>L : E →L[𝕜] F<VAR>r : ℝ<VAR>ε δ : ℝ<VAR>h : ε ≤ δ<GOAL>FDerivMeasurableAux.A f L r ε ⊆ FDerivMeasurableAux.A f L r δ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>r ε : ℝ<VAR>L : E →L[𝕜] F<VAR>x : E<VAR>hx : x ∈ FDerivMeasurableAux.A f L r ε<VAR>y z : E<VAR>hy : y ∈ Metric.closedBall x (r / 2)<VAR>hz : z ∈ Metric.closedBall x (r / 2)<GOAL>‖f z - f y - L (z - y)‖ ≤ ε * r
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>x : E<VAR>hx : DifferentiableAt 𝕜 f x<GOAL>∃ R > 0, ∀ r ∈ Set.Ioo 0 R, x ∈ FDerivMeasurableAux.A f (fderiv 𝕜 f x) r ε
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>r ε : ℝ<VAR>hε : 0 < ε<VAR>hr : 0 < r<VAR>x : E<VAR>L₁ L₂ : E →L[𝕜] F<VAR>h₁ : x ∈ FDerivMeasurableAux.A f L₁ r ε<VAR>h₂ : x ∈ FDerivMeasurableAux.A f L₂ r ε<GOAL>‖L₁ - L₂‖ ≤ 4 * ‖c‖ * ε
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<GOAL>{x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} ⊆ FDerivMeasurableAux.D f K
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<GOAL>FDerivMeasurableAux.D f K ⊆ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<GOAL>{x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} = FDerivMeasurableAux.D f K
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<GOAL>MeasurableSet {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>CompleteSpace F<GOAL>MeasurableSet {x | DifferentiableAt 𝕜 f x}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>CompleteSpace F<GOAL>Measurable (fderiv 𝕜 f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>CompleteSpace F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>y : E<GOAL>Measurable fun x => (fderiv 𝕜 f x) y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>MeasurableSpace 𝕜<VAR>OpensMeasurableSpace 𝕜<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>f : 𝕜 → F<GOAL>Measurable (deriv f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>MeasurableSpace 𝕜<VAR>OpensMeasurableSpace 𝕜<VAR>h : SecondCountableTopologyEither 𝕜 F<VAR>f : 𝕜 → F<GOAL>MeasureTheory.StronglyMeasurable (deriv f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>MeasurableSpace 𝕜<VAR>OpensMeasurableSpace 𝕜<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>f : 𝕜 → F<VAR>μ : MeasureTheory.Measure 𝕜<GOAL>AEMeasurable (deriv f) μ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>MeasurableSpace 𝕜<VAR>OpensMeasurableSpace 𝕜<VAR>SecondCountableTopologyEither 𝕜 F<VAR>f : 𝕜 → F<VAR>μ : MeasureTheory.Measure 𝕜<GOAL>MeasureTheory.AEStronglyMeasurable (deriv f) μ
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>L : F<VAR>r ε x : ℝ<VAR>hx : x ∈ RightDerivMeasurableAux.A f L r ε<GOAL>RightDerivMeasurableAux.A f L r ε ∈ 𝓝[>] x
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>r s ε x : ℝ<VAR>hx : x ∈ RightDerivMeasurableAux.B f K r s ε<GOAL>RightDerivMeasurableAux.B f K r s ε ∈ 𝓝[>] x
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>r s ε : ℝ<GOAL>MeasurableSet (RightDerivMeasurableAux.B f K r s ε)
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>L : F<VAR>r : ℝ<VAR>ε δ : ℝ<VAR>h : ε ≤ δ<GOAL>RightDerivMeasurableAux.A f L r ε ⊆ RightDerivMeasurableAux.A f L r δ
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>r ε : ℝ<VAR>L : F<VAR>x : ℝ<VAR>hx : x ∈ RightDerivMeasurableAux.A f L r ε<VAR>y z : ℝ<VAR>hy : y ∈ Set.Icc x (x + r / 2)<VAR>hz : z ∈ Set.Icc x (x + r / 2)<GOAL>‖f z - f y - (z - y) • L‖ ≤ ε * r
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>x : ℝ<VAR>hx : DifferentiableWithinAt ℝ f (Set.Ici x) x<GOAL>∃ R > 0, ∀ r ∈ Set.Ioo 0 R, x ∈ RightDerivMeasurableAux.A f (derivWithin f (Set.Ici x) x) r ε
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>r x : ℝ<VAR>hr : 0 < r<VAR>ε : ℝ<VAR>L₁ L₂ : F<VAR>h₁ : x ∈ RightDerivMeasurableAux.A f L₁ r ε<VAR>h₂ : x ∈ RightDerivMeasurableAux.A f L₂ r ε<GOAL>‖L₁ - L₂‖ ≤ 4 * ε
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<GOAL>{x | DifferentiableWithinAt ℝ f (Set.Ici x) x ∧ derivWithin f (Set.Ici x) x ∈ K} ⊆ RightDerivMeasurableAux.D f K
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>hK : IsComplete K<GOAL>RightDerivMeasurableAux.D f K ⊆ {x | DifferentiableWithinAt ℝ f (Set.Ici x) x ∧ derivWithin f (Set.Ici x) x ∈ K}
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>hK : IsComplete K<GOAL>{x | DifferentiableWithinAt ℝ f (Set.Ici x) x ∧ derivWithin f (Set.Ici x) x ∈ K} = RightDerivMeasurableAux.D f K
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>hK : IsComplete K<GOAL>MeasurableSet {x | DifferentiableWithinAt ℝ f (Set.Ici x) x ∧ derivWithin f (Set.Ici x) x ∈ K}
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>CompleteSpace F<GOAL>MeasurableSet {x | DifferentiableWithinAt ℝ f (Set.Ici x) x}
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>CompleteSpace F<VAR>MeasurableSpace F<VAR>BorelSpace F<GOAL>Measurable fun x => derivWithin f (Set.Ici x) x
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>CompleteSpace F<GOAL>MeasureTheory.StronglyMeasurable fun x => derivWithin f (Set.Ici x) x
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>CompleteSpace F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>μ : MeasureTheory.Measure ℝ<GOAL>AEMeasurable (fun x => derivWithin f (Set.Ici x) x) μ
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>CompleteSpace F<VAR>μ : MeasureTheory.Measure ℝ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => derivWithin f (Set.Ici x) x) μ
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>CompleteSpace F<GOAL>MeasurableSet {x | DifferentiableWithinAt ℝ f (Set.Ioi x) x}
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>CompleteSpace F<VAR>MeasurableSpace F<VAR>BorelSpace F<GOAL>Measurable fun x => derivWithin f (Set.Ioi x) x
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>CompleteSpace F<GOAL>MeasureTheory.StronglyMeasurable fun x => derivWithin f (Set.Ioi x) x
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>CompleteSpace F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>μ : MeasureTheory.Measure ℝ<GOAL>AEMeasurable (fun x => derivWithin f (Set.Ioi x) x) μ
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>CompleteSpace F<VAR>μ : MeasureTheory.Measure ℝ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => derivWithin f (Set.Ioi x) x) μ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>LocallyCompactSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>f : α → E → F<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<GOAL>IsOpen {p | p.2 ∈ FDerivMeasurableAux.A (f p.1) L r s}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>LocallyCompactSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>f : α → E → F<VAR>r s t : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<GOAL>IsOpen {p | p.2 ∈ FDerivMeasurableAux.B (f p.1) K r s t}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>LocallyCompactSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace α<VAR>OpensMeasurableSpace E<VAR>f : α → E → F<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<GOAL>MeasurableSet {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>LocallyCompactSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace α<VAR>OpensMeasurableSpace E<VAR>f : α → E → F<VAR>CompleteSpace F<VAR>hf : Continuous (Function.uncurry f)<GOAL>MeasurableSet {p | DifferentiableAt 𝕜 (f p.1) p.2}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>LocallyCompactSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace α<VAR>OpensMeasurableSpace E<VAR>f : α → E → F<VAR>CompleteSpace F<VAR>hf : Continuous (Function.uncurry f)<GOAL>Measurable fun p => fderiv 𝕜 (f p.1) p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>LocallyCompactSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace α<VAR>OpensMeasurableSpace E<VAR>f : α → E → F<VAR>CompleteSpace F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>hf : Continuous (Function.uncurry f)<VAR>y : E<GOAL>Measurable fun p => (fderiv 𝕜 (f p.1) p.2) y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>CompleteSpace F<VAR>LocallyCompactSpace 𝕜<VAR>MeasurableSpace 𝕜<VAR>OpensMeasurableSpace 𝕜<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>f : α → 𝕜 → F<VAR>hf : Continuous (Function.uncurry f)<GOAL>Measurable fun p => deriv (f p.1) p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>CompleteSpace F<VAR>LocallyCompactSpace 𝕜<VAR>MeasurableSpace 𝕜<VAR>OpensMeasurableSpace 𝕜<VAR>h : SecondCountableTopologyEither α F<VAR>f : α → 𝕜 → F<VAR>hf : Continuous (Function.uncurry f)<GOAL>MeasureTheory.StronglyMeasurable fun p => deriv (f p.1) p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>CompleteSpace F<VAR>LocallyCompactSpace 𝕜<VAR>MeasurableSpace 𝕜<VAR>OpensMeasurableSpace 𝕜<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>f : α → 𝕜 → F<VAR>hf : Continuous (Function.uncurry f)<VAR>μ : MeasureTheory.Measure (α × 𝕜)<GOAL>AEMeasurable (fun p => deriv (f p.1) p.2) μ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>CompleteSpace F<VAR>LocallyCompactSpace 𝕜<VAR>MeasurableSpace 𝕜<VAR>OpensMeasurableSpace 𝕜<VAR>SecondCountableTopologyEither α F<VAR>f : α → 𝕜 → F<VAR>hf : Continuous (Function.uncurry f)<VAR>μ : MeasureTheory.Measure (α × 𝕜)<GOAL>MeasureTheory.AEStronglyMeasurable (fun p => deriv (f p.1) p.2) μ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>Y : C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n b q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : AlgebraicTopology.DoldKan.HigherFacesVanish q φ<VAR>hnbq : n + 1 = b + q<GOAL>AlgebraicTopology.DoldKan.HigherFacesVanish q (φ ≫ X.σ ⟨b, ⋯⟩)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n q : ℕ<VAR>i : Fin (n + 1)<VAR>hi : n + 1 ≤ ↑i + q<GOAL>X.σ i ≫ (AlgebraicTopology.DoldKan.P q).f (n + 1) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.σ i ≫ AlgebraicTopology.DoldKan.PInfty.f (n + 1) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : [n] ⟶ Δ'<VAR>hθ : ¬CategoryTheory.Mono θ<GOAL>X.map θ.op ≫ AlgebraicTopology.DoldKan.PInfty.f n = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>i : ℕ<GOAL>(AlgebraicTopology.DoldKan.Γ₀NondegComplexIso K).inv.f i = 𝟙 ((AlgebraicTopology.DoldKan.Γ₀.splitting K).N i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>i : ℕ<GOAL>(AlgebraicTopology.DoldKan.Γ₀NondegComplexIso K).hom.f i = 𝟙 ((AlgebraicTopology.DoldKan.Γ₀.splitting K).N i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<GOAL>AlgebraicTopology.DoldKan.N₁Γ₀.app K = (AlgebraicTopology.DoldKan.Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫ (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).mapIso (AlgebraicTopology.DoldKan.Γ₀NondegComplexIso K)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<GOAL>AlgebraicTopology.DoldKan.N₁Γ₀.hom.app K = (AlgebraicTopology.DoldKan.Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).map (AlgebraicTopology.DoldKan.Γ₀NondegComplexIso K).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<GOAL>AlgebraicTopology.DoldKan.N₁Γ₀.inv.app K = (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).map (AlgebraicTopology.DoldKan.Γ₀NondegComplexIso K).inv ≫ (AlgebraicTopology.DoldKan.Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<GOAL>(AlgebraicTopology.DoldKan.N₁Γ₀.hom.app K).f.f n = (AlgebraicTopology.DoldKan.Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv.f.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<GOAL>(AlgebraicTopology.DoldKan.N₁Γ₀.inv.app K).f.f n = (AlgebraicTopology.DoldKan.Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom.f.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<GOAL>(AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso.hom.app X).f = AlgebraicTopology.DoldKan.PInfty
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<GOAL>(AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso.inv.app X).f = AlgebraicTopology.DoldKan.PInfty
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)<VAR>n : ℕ<GOAL>(AlgebraicTopology.DoldKan.N₂Γ₂.inv.app X).f.f n = X.p.f n ≫ ((AlgebraicTopology.DoldKan.Γ₀.splitting X.X).cofan (Opposite.op [n])).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op [n]))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>CategoryTheory.whiskerLeft (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)) AlgebraicTopology.DoldKan.N₂Γ₂.hom = AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso.hom ≫ AlgebraicTopology.DoldKan.N₁Γ₀.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<GOAL>AlgebraicTopology.DoldKan.N₂Γ₂.hom.app ((CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).obj K) = AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso.hom.app K ≫ AlgebraicTopology.DoldKan.N₁Γ₀.hom.app K