ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>N : Type u_6<VAR>inst✝⁷ : Monoid R<VAR>inst✝⁶ : Monoid S<VAR>σ : R → S<VAR>inst✝⁵ : MulAction R M<VAR>inst✝⁴ : MulAction S N<VAR>inst✝³ : MulAction R M₁<VAR>inst✝² : MulAction R M₂<VAR>F : Type u_7<VAR>h : F<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MulActionSemiHomClass F σ M N<VAR>c : R<VAR>s : Set M<VAR>t : Set N<VAR>hc : Function.Surjective fun m => c • m<VAR>hc' : Function.Injective fun n => σ c • n<GOAL>c • ⇑h ⁻¹' t ≤ ⇑h ⁻¹' (σ c • t)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁵ : SeminormedAddCommGroup E<VAR>inst✝¹⁴ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹³ : SeminormedAddCommGroup F<VAR>inst✝¹² : SeminormedAddCommGroup Fₗ<VAR>inst✝¹¹ : SeminormedAddCommGroup G<VAR>inst✝¹⁰ : SeminormedAddCommGroup Gₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>inst✝³ : NormedSpace 𝕜 Fₗ<VAR>inst✝² : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝ : FunLike 𝓕 E F<VAR>f : E →SL[σ₁₂] F<VAR>M : ℝ<VAR>hMp : 0 ≤ M<VAR>hM : ∀ (x : E), ‖x‖ ≠ 0 → ‖f x‖ ≤ M * ‖x‖<VAR>x : E<VAR>h : ‖x‖ = 0<GOAL>‖f x‖ ≤ M * ‖x‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>x : ℝ<VAR>s : ℂ<VAR>f : E<GOAL>↑(rexp (-x)) • cexp (-↑x) ^ (s - 1) • f = cexp (-s * ↑x) • f
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>x : ℝ<VAR>s : ℂ<VAR>f : E<GOAL>(↑(rexp (-x)) * cexp (-↑x) ^ (s - 1)) • f = cexp (-s * ↑x) • f
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>x : ℝ<VAR>s : ℂ<VAR>f : E<GOAL>(cexp (-↑x) * cexp (-↑x) ^ (s - 1)) • f = cexp (-s * ↑x) • f
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>x : ℝ<VAR>s : ℂ<VAR>f : E<GOAL>(cexp (-↑x) ^ 1 * cexp (-↑x) ^ (s - 1)) • f = cexp (-s * ↑x) • f
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>x : ℝ<VAR>s : ℂ<VAR>f : E<GOAL>cexp (-↑x * (1 + (s - 1))) • f = cexp (-s * ↑x) • f
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>z * (starRingEnd K) z = ↑‖z‖ ^ 2
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x✝ y✝ z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<VAR>x y : X<GOAL>dist x y = dist (inl x) (inl y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x✝ y✝ z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<VAR>x y : X<GOAL>dist x y = Sum.dist (inl x) (inl y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x✝ y✝ z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<VAR>x y : X<GOAL>1 ≤ ↑(GromovHausdorff.maxVar X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x✝ y✝ z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<VAR>x : X<VAR>y : Y<GOAL>1 ≤ dist (inl x) (inr y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x✝ y✝ z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<VAR>x : Y<VAR>y : X<GOAL>1 ≤ dist (inl x) (inr y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x✝ y✝ z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<VAR>x y : Y<GOAL>dist x y = dist (inr x) (inr y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x✝ y✝ z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<VAR>x y : Y<GOAL>dist x y = Sum.dist (inr x) (inr y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x✝ y✝ z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<VAR>x y : Y<GOAL>1 ≤ ↑(GromovHausdorff.maxVar X Y)
<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✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>x✝ : E<VAR>s : Set (Seminorm 𝕜 E)<VAR>hp : BddAbove s<VAR>x : E<GOAL>(sSup s) x = ⨆ p, ↑p x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<GOAL>IsOpen {p | p.2 ∈ A (f p.1) L r s}
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this : ProperSpace E<GOAL>IsOpen {p | p.2 ∈ A (f p.1) L r s}
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this : ProperSpace E<GOAL>IsOpen {p | ∃ r', (r / 2 < r' ∧ r' ≤ r) ∧ ∀ (y : E), dist y p.2 < r' → ∀ (z : E), dist z p.2 < r' → ‖f p.1 z - f p.1 y - (L z - L y)‖ < s * r}
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this : ProperSpace E<GOAL>∀ x ∈ {p | ∃ r', (r / 2 < r' ∧ r' ≤ r) ∧ ∀ (y : E), dist y p.2 < r' → ∀ (z : E), dist z p.2 < r' → ‖f p.1 z - f p.1 y - (L z - L y)‖ < s * r}, {p | ∃ r', (r / 2 < r' ∧ r' ≤ r) ∧ ∀ (y : E), dist y p.2 < r' → ∀ (z : E), dist z p.2 < r' → ‖f p.1 z - f p.1 y - (L z - L y)‖ < s * r} ∈ 𝓝 x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this : ProperSpace E<VAR>a : α<VAR>x : E<VAR>r' : ℝ<VAR>hr : ∀ (y : E), dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r<VAR>Irr' : r / 2 < r'<VAR>Ir'r : r' ≤ r<GOAL>{p | ∃ r', (r / 2 < r' ∧ r' ≤ r) ∧ ∀ (y : E), dist y p.2 < r' → ∀ (z : E), dist z p.2 < r' → ‖f p.1 z - f p.1 y - (L z - L y)‖ < s * r} ∈ 𝓝 (a, x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this : ProperSpace E<VAR>a : α<VAR>x : E<VAR>r' : ℝ<VAR>hr : ∀ (y : E), dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r<VAR>Irr' : r / 2 < r'<VAR>Ir'r : r' ≤ r<VAR>ha : Continuous (f a)<GOAL>{p | ∃ r', (r / 2 < r' ∧ r' ≤ r) ∧ ∀ (y : E), dist y p.2 < r' → ∀ (z : E), dist z p.2 < r' → ‖f p.1 z - f p.1 y - (L z - L y)‖ < s * r} ∈ 𝓝 (a, x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this : ProperSpace E<VAR>a : α<VAR>x : E<VAR>r' : ℝ<VAR>hr : ∀ (y : E), dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r<VAR>Irr' : r / 2 < r'<VAR>Ir'r : r' ≤ r<VAR>ha : Continuous (f a)<VAR>t : ℝ<VAR>hrt : r / 2 < t<VAR>htr' : t < r'<GOAL>{p | ∃ r', (r / 2 < r' ∧ r' ≤ r) ∧ ∀ (y : E), dist y p.2 < r' → ∀ (z : E), dist z p.2 < r' → ‖f p.1 z - f p.1 y - (L z - L y)‖ < s * r} ∈ 𝓝 (a, x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this : ProperSpace E<VAR>a : α<VAR>x : E<VAR>r' : ℝ<VAR>hr : ∀ (y : E), dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r<VAR>Irr' : r / 2 < r'<VAR>Ir'r : r' ≤ r<VAR>ha : Continuous (f a)<VAR>t : ℝ<VAR>hrt : r / 2 < t<VAR>htr' : t < r'<VAR>t' : ℝ<VAR>hrt' : r / 2 < t'<VAR>ht't : t' < t<GOAL>{p | ∃ r', (r / 2 < r' ∧ r' ≤ r) ∧ ∀ (y : E), dist y p.2 < r' → ∀ (z : E), dist z p.2 < r' → ‖f p.1 z - f p.1 y - (L z - L y)‖ < s * r} ∈ 𝓝 (a, x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this : ProperSpace E<VAR>a : α<VAR>x : E<VAR>r' : ℝ<VAR>hr : ∀ (y : E), dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r<VAR>Irr' : r / 2 < r'<VAR>Ir'r : r' ≤ r<VAR>ha : Continuous (f a)<VAR>t : ℝ<VAR>hrt : r / 2 < t<VAR>htr' : t < r'<VAR>t' : ℝ<VAR>hrt' : r / 2 < t'<VAR>ht't : t' < t<VAR>b : ℝ<VAR>b_lt : b < s * r<VAR>hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b<GOAL>{p | ∃ r', (r / 2 < r' ∧ r' ≤ r) ∧ ∀ (y : E), dist y p.2 < r' → ∀ (z : E), dist z p.2 < r' → ‖f p.1 z - f p.1 y - (L z - L y)‖ < s * r} ∈ 𝓝 (a, x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this : ProperSpace E<VAR>a : α<VAR>x : E<VAR>r' : ℝ<VAR>hr : ∀ (y : E), dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r<VAR>Irr' : r / 2 < r'<VAR>Ir'r : r' ≤ r<VAR>ha : Continuous (f a)<VAR>t : ℝ<VAR>hrt : r / 2 < t<VAR>htr' : t < r'<VAR>t' : ℝ<VAR>hrt' : r / 2 < t'<VAR>ht't : t' < t<VAR>b : ℝ<VAR>b_lt : b < s * r<VAR>hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : b + 2 * ε < s * r<GOAL>{p | ∃ r', (r / 2 < r' ∧ r' ≤ r) ∧ ∀ (y : E), dist y p.2 < r' → ∀ (z : E), dist z p.2 < r' → ‖f p.1 z - f p.1 y - (L z - L y)‖ < s * r} ∈ 𝓝 (a, x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this : ProperSpace E<VAR>a : α<VAR>x : E<VAR>r' : ℝ<VAR>hr : ∀ (y : E), dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r<VAR>Irr' : r / 2 < r'<VAR>Ir'r : r' ≤ r<VAR>ha : Continuous (f a)<VAR>t : ℝ<VAR>hrt : r / 2 < t<VAR>htr' : t < r'<VAR>t' : ℝ<VAR>hrt' : r / 2 < t'<VAR>ht't : t' < t<VAR>b : ℝ<VAR>b_lt : b < s * r<VAR>hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : b + 2 * ε < s * r<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>au : a ∈ u<VAR>hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε<GOAL>{p | ∃ r', (r / 2 < r' ∧ r' ≤ r) ∧ ∀ (y : E), dist y p.2 < r' → ∀ (z : E), dist z p.2 < r' → ‖f p.1 z - f p.1 y - (L z - L y)‖ < s * r} ∈ 𝓝 (a, x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this✝ : ProperSpace E<VAR>a : α<VAR>x : E<VAR>r' : ℝ<VAR>hr : ∀ (y : E), dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r<VAR>Irr' : r / 2 < r'<VAR>Ir'r : r' ≤ r<VAR>ha : Continuous (f a)<VAR>t : ℝ<VAR>hrt : r / 2 < t<VAR>htr' : t < r'<VAR>t' : ℝ<VAR>hrt' : r / 2 < t'<VAR>ht't : t' < t<VAR>b : ℝ<VAR>b_lt : b < s * r<VAR>hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : b + 2 * ε < s * r<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>au : a ∈ u<VAR>hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε<VAR>this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)<GOAL>{p | ∃ r', (r / 2 < r' ∧ r' ≤ r) ∧ ∀ (y : E), dist y p.2 < r' → ∀ (z : E), dist z p.2 < r' → ‖f p.1 z - f p.1 y - (L z - L y)‖ < s * r} ∈ 𝓝 (a, x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this✝ : ProperSpace E<VAR>a : α<VAR>x : E<VAR>r' : ℝ<VAR>hr : ∀ (y : E), dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r<VAR>Irr' : r / 2 < r'<VAR>Ir'r : r' ≤ r<VAR>ha : Continuous (f a)<VAR>t : ℝ<VAR>hrt : r / 2 < t<VAR>htr' : t < r'<VAR>t' : ℝ<VAR>hrt' : r / 2 < t'<VAR>ht't : t' < t<VAR>b : ℝ<VAR>b_lt : b < s * r<VAR>hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : b + 2 * ε < s * r<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>au : a ∈ u<VAR>hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε<VAR>this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)<GOAL>∀ a ∈ u ×ˢ ball x (t - t'), ∃ r', (r / 2 < r' ∧ r' ≤ r) ∧ ∀ (y : E), dist y a.2 < r' → ∀ (z : E), dist z a.2 < r' → ‖f a.1 z - f a.1 y - (L z - L y)‖ < s * r
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this✝ : ProperSpace E<VAR>a : α<VAR>x : E<VAR>r' : ℝ<VAR>hr : ∀ (y : E), dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r<VAR>Irr' : r / 2 < r'<VAR>Ir'r : r' ≤ r<VAR>ha : Continuous (f a)<VAR>t : ℝ<VAR>hrt : r / 2 < t<VAR>htr' : t < r'<VAR>t' : ℝ<VAR>hrt' : r / 2 < t'<VAR>ht't : t' < t<VAR>b : ℝ<VAR>b_lt : b < s * r<VAR>hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : b + 2 * ε < s * r<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>au : a ∈ u<VAR>hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε<VAR>this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)<VAR>a' : α<VAR>x' : E<VAR>ha'x' : (a', x') ∈ u ×ˢ ball x (t - t')<GOAL>∃ r', (r / 2 < r' ∧ r' ≤ r) ∧ ∀ (y : E), dist y (a', x').2 < r' → ∀ (z : E), dist z (a', x').2 < r' → ‖f (a', x').1 z - f (a', x').1 y - (L z - L y)‖ < s * r
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this✝ : ProperSpace E<VAR>a : α<VAR>x : E<VAR>r' : ℝ<VAR>hr : ∀ (y : E), dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r<VAR>Irr' : r / 2 < r'<VAR>Ir'r : r' ≤ r<VAR>ha : Continuous (f a)<VAR>t : ℝ<VAR>hrt : r / 2 < t<VAR>htr' : t < r'<VAR>t' : ℝ<VAR>hrt' : r / 2 < t'<VAR>ht't : t' < t<VAR>b : ℝ<VAR>b_lt : b < s * r<VAR>hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : b + 2 * ε < s * r<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>au : a ∈ u<VAR>hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε<VAR>this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)<VAR>a' : α<VAR>x' : E<VAR>ha'x' : a' ∈ u ∧ dist x' x < t - t'<GOAL>∃ r', (r / 2 < r' ∧ r' ≤ r) ∧ ∀ (y : E), dist y (a', x').2 < r' → ∀ (z : E), dist z (a', x').2 < r' → ‖f (a', x').1 z - f (a', x').1 y - (L z - L y)‖ < s * r
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this✝ : ProperSpace E<VAR>a : α<VAR>x : E<VAR>r' : ℝ<VAR>hr : ∀ (y : E), dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r<VAR>Irr' : r / 2 < r'<VAR>Ir'r : r' ≤ r<VAR>ha : Continuous (f a)<VAR>t : ℝ<VAR>hrt : r / 2 < t<VAR>htr' : t < r'<VAR>t' : ℝ<VAR>hrt' : r / 2 < t'<VAR>ht't : t' < t<VAR>b : ℝ<VAR>b_lt : b < s * r<VAR>hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : b + 2 * ε < s * r<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>au : a ∈ u<VAR>hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε<VAR>this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)<VAR>a' : α<VAR>x' : E<VAR>ha'x' : a' ∈ u ∧ dist x' x < t - t'<VAR>y : E<VAR>hy : dist y (a', x').2 < t'<VAR>z : E<VAR>hz : dist z (a', x').2 < t'<GOAL>‖f (a', x').1 z - f (a', x').1 y - (L z - L y)‖ < s * r