ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂<GOAL>Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂<GOAL>Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ ≠ 0<GOAL>Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
<VAR>x✝ y x : ℝ<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : x ≤ 1<GOAL>sin (arccos x) = √(1 - x ^ 2)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : SemilatticeSup β<VAR>p : α × β → Prop<VAR>hp : ∀ᶠ (x : α × β) in atTop, p x<GOAL>∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : SemilatticeSup β<VAR>p : α × β → Prop<VAR>hp : ∀ᶠ (x : α × β) in atTop ×ˢ atTop, p x<GOAL>∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I✝ J : Ideal R<VAR>N P : Submodule R M<VAR>I : Ideal R<VAR>f : R →ₗ[R] M<VAR>y : R<VAR>hy : y ∈ ↑I<GOAL>f y ∈ I • ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I✝ J : Ideal R<VAR>N P : Submodule R M<VAR>I : Ideal R<VAR>f : R →ₗ[R] M<VAR>y : R<VAR>hy : y ∈ ↑I<GOAL>y • f 1 ∈ I • ⊤
<VAR>α : Type u<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>f✝ : α → R<VAR>f : FreeCommRing α →+* R<VAR>x : FreeCommRing α<GOAL>(lift (⇑f ∘ of)) (-1) = f (-1)
<VAR>α : Type u<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>f✝ : α → R<VAR>f : FreeCommRing α →+* R<VAR>x✝ x y : FreeCommRing α<VAR>ihx : (lift (⇑f ∘ of)) x = f x<VAR>ihy : (lift (⇑f ∘ of)) y = f y<GOAL>(lift (⇑f ∘ of)) (x + y) = f (x + y)
<VAR>α : Type u<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>f✝ : α → R<VAR>f : FreeCommRing α →+* R<VAR>x✝ x y : FreeCommRing α<VAR>ihx : (lift (⇑f ∘ of)) x = f x<VAR>ihy : (lift (⇑f ∘ of)) y = f y<GOAL>(lift (⇑f ∘ of)) (x * y) = f (x * y)
<VAR>α : Type u_1<VAR>d : DynkinSystem α<VAR>a : Set α<VAR>h : d.Has aᶜ<GOAL>d.Has a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>t s : Set A<VAR>h : t ⊆ s<VAR>hx : AlgebraicIndependent R Subtype.val<GOAL>AlgebraicIndependent R Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>f g : α →ₛ β<GOAL>↑(piecewise ∅ ⋯ f g) = ↑g
<VAR>D : GlueData<VAR>i : D.J<VAR>U : Opens ↑(D.U i)<GOAL>IsOpen (⇑(D.ι i) '' ↑U)
<VAR>D : GlueData<VAR>i : D.J<VAR>U : Opens ↑(D.U i)<GOAL>∀ (i_1 : D.J), IsOpen (⇑(D.ι i_1) ⁻¹' (⇑(D.ι i) '' ↑U))
<VAR>D : GlueData<VAR>i : D.J<VAR>U : Opens ↑(D.U i)<VAR>j : D.J<GOAL>IsOpen (⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' ↑U))
<VAR>D : GlueData<VAR>i : D.J<VAR>U : Opens ↑(D.U i)<VAR>j : D.J<GOAL>IsOpen (⇑(D.f j i) '' (⇑(D.t j i ≫ D.f i j) ⁻¹' ↑U))
<VAR>D : GlueData<VAR>i : D.J<VAR>U : Opens ↑(D.U i)<VAR>j : D.J<GOAL>IsOpen (⇑(D.t j i ≫ D.f i j) ⁻¹' ↑U)
<VAR>D : GlueData<VAR>i : D.J<VAR>U : Opens ↑(D.U i)<VAR>j : D.J<GOAL>IsOpen ↑U
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>x y : ι → ℝ<VAR>I J : WithBot (Box ι)<GOAL>Disjoint ↑I ↑J ↔ Disjoint I J
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>x y : ι → ℝ<VAR>I J : WithBot (Box ι)<GOAL>↑I ⊓ ↑J ≤ ⊥ ↔ ↑I ∩ ↑J ⊆ ↑⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>h : ∀ (s : Set α), MeasurableSet s → μ₁ s = μ₂ s<GOAL>μ₁.toOuterMeasure = μ₂.toOuterMeasure
<VAR>K : Type u<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : IsDomain K<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>inst✝¹ : DistribMulAction R K[X]<VAR>inst✝ : IsScalarTower R K[X] K[X]<VAR>c : R<VAR>p q : K[X]<GOAL>(algebraMap K[X] (RatFunc K)) (c • p) / (algebraMap K[X] (RatFunc K)) q = c • ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q)
<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>A✝ A : ValuationSubring K<VAR>P : Ideal ↥A<VAR>inst✝ : P.IsPrime<GOAL>A.idealOfLE (A.ofPrime P) ⋯ = P
<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>A✝ A : ValuationSubring K<VAR>P : Ideal ↥A<VAR>inst✝ : P.IsPrime<VAR>x : ↥A<GOAL>x ∈ A.idealOfLE (A.ofPrime P) ⋯ ↔ x ∈ P
<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>A✝ A : ValuationSubring K<VAR>P : Ideal ↥A<VAR>inst✝ : P.IsPrime<VAR>x : ↥A<GOAL>optParam (LocalRing ↥(A.ofPrime P)) ⋯
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z : R<VAR>a✝ b✝ c a b : ℍ[R]<GOAL>normSq (a + b) = normSq a + (a * star b).re + ((b * star a).re + normSq b)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z : R<VAR>a✝ b✝ c a b : ℍ[R]<GOAL>normSq a + normSq b + ((a * star b).re + (b * star a).re) = normSq a + normSq b + 2 * (a * star b).re
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w : E<VAR>hv : x + v ∈ interior s<VAR>hw : x + v + w ∈ interior s<GOAL>(fun h => f (x + h • v + h • w) - f (x + h • v) - h • (f' x) w - h ^ 2 • (f'' v) w - (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0] fun h => h ^ 2
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w : E<VAR>hv : x + v ∈ interior s<VAR>hw : x + v + w ∈ interior s<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∀ᶠ (x_1 : ℝ) in 𝓝[>] 0, ‖f (x + x_1 • v + x_1 • w) - f (x + x_1 • v) - x_1 • (f' x) w - x_1 ^ 2 • (f'' v) w - (x_1 ^ 2 / 2) • (f'' w) w‖ ≤ ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * x_1 ^ 2‖
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖<VAR>v w : E<VAR>hv : x + v ∈ interior s<VAR>hw : x + v + w ∈ interior s<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∀ᶠ (x_1 : ℝ) in 𝓝[>] 0, ‖f (x + x_1 • v + x_1 • w) - f (x + x_1 • v) - x_1 • (f' x) w - x_1 ^ 2 • (f'' v) w - (x_1 ^ 2 / 2) • (f'' w) w‖ ≤ ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * x_1 ^ 2‖
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖<VAR>v w : E<VAR>hv : x + v ∈ interior s<VAR>hw : x + v + w ∈ interior s<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 => ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}<GOAL>∀ᶠ (x_1 : ℝ) in 𝓝[>] 0, ‖f (x + x_1 • v + x_1 • w) - f (x + x_1 • v) - x_1 • (f' x) w - x_1 ^ 2 • (f'' v) w - (x_1 ^ 2 / 2) • (f'' w) w‖ ≤ ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * x_1 ^ 2‖
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖<VAR>v w : E<VAR>hv : x + v ∈ interior s<VAR>hw : x + v + w ∈ interior s<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 => ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}<VAR>E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ<GOAL>∀ᶠ (x_1 : ℝ) in 𝓝[>] 0, ‖f (x + x_1 • v + x_1 • w) - f (x + x_1 • v) - x_1 • (f' x) w - x_1 ^ 2 • (f'' v) w - (x_1 ^ 2 / 2) • (f'' w) w‖ ≤ ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * x_1 ^ 2‖
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖<VAR>v w : E<VAR>hv : x + v ∈ interior s<VAR>hw : x + v + w ∈ interior s<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 => ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}<VAR>E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ<VAR>E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1<GOAL>∀ᶠ (x_1 : ℝ) in 𝓝[>] 0, ‖f (x + x_1 • v + x_1 • w) - f (x + x_1 • v) - x_1 • (f' x) w - x_1 ^ 2 • (f'' v) w - (x_1 ^ 2 / 2) • (f'' w) w‖ ≤ ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * x_1 ^ 2‖
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖<VAR>v w : E<VAR>hv : x + v ∈ interior s<VAR>hw : x + v + w ∈ interior s<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 => ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}<VAR>E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ<VAR>E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1<VAR>h : ℝ<VAR>hδ : h * (‖v‖ + ‖w‖) < δ<VAR>h_lt_1 : h < 1<VAR>hpos : h ∈ Ioi 0<GOAL>‖f (x + h • v + h • w) - f (x + h • v) - h • (f' x) w - h ^ 2 • (f'' v) w - (h ^ 2 / 2) • (f'' w) w‖ ≤ ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * h ^ 2‖
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖<VAR>v w : E<VAR>hv : x + v ∈ interior s<VAR>hw : x + v + w ∈ interior s<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 => ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}<VAR>E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ<VAR>E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1<VAR>h : ℝ<VAR>hδ : h * (‖v‖ + ‖w‖) < δ<VAR>h_lt_1 : h < 1<VAR>hpos : 0 < h<GOAL>‖f (x + h • v + h • w) - f (x + h • v) - h • (f' x) w - h ^ 2 • (f'' v) w - (h ^ 2 / 2) • (f'' w) w‖ ≤ ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * h ^ 2‖
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖<VAR>v w : E<VAR>hv : x + v ∈ interior s<VAR>hw : x + v + w ∈ interior s<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 => ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}<VAR>E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ<VAR>E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1<VAR>h : ℝ<VAR>hδ : h * (‖v‖ + ‖w‖) < δ<VAR>h_lt_1 : h < 1<VAR>hpos : 0 < h<VAR>xt_mem : ∀ t ∈ Icc 0 1, x + h • v + (t * h) • w ∈ interior s<GOAL>‖f (x + h • v + h • w) - f (x + h • v) - h • (f' x) w - h ^ 2 • (f'' v) w - (h ^ 2 / 2) • (f'' w) w‖ ≤ ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * h ^ 2‖
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖<VAR>v w : E<VAR>hv : x + v ∈ interior s<VAR>hw : x + v + w ∈ interior s<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 => ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}<VAR>E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ<VAR>E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1<VAR>h : ℝ<VAR>hδ : h * (‖v‖ + ‖w‖) < δ<VAR>h_lt_1 : h < 1<VAR>hpos : 0 < h<VAR>xt_mem : ∀ t ∈ Icc 0 1, x + h • v + (t * h) • w ∈ interior s<VAR>g : ℝ → F := fun t => f (x + h • v + (t * h) • w) - (t * h) • (f' x) w - (t * h ^ 2) • (f'' v) w - ((t * h) ^ 2 / 2) • (f'' w) w<VAR>g' : ℝ → F := fun t => (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w<VAR>hg' : g' = fun t => (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w<VAR>g_deriv : ∀ t ∈ Icc 0 1, HasDerivWithinAt g (g' t) (Icc 0 1) t<GOAL>‖f (x + h • v + h • w) - f (x + h • v) - h • (f' x) w - h ^ 2 • (f'' v) w - (h ^ 2 / 2) • (f'' w) w‖ ≤ ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * h ^ 2‖
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖<VAR>v w : E<VAR>hv : x + v ∈ interior s<VAR>hw : x + v + w ∈ interior s<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 => ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}<VAR>E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ<VAR>E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1<VAR>h : ℝ<VAR>hδ : h * (‖v‖ + ‖w‖) < δ<VAR>h_lt_1 : h < 1<VAR>hpos : 0 < h<VAR>xt_mem : ∀ t ∈ Icc 0 1, x + h • v + (t * h) • w ∈ interior s<VAR>g : ℝ → F := fun t => f (x + h • v + (t * h) • w) - (t * h) • (f' x) w - (t * h ^ 2) • (f'' v) w - ((t * h) ^ 2 / 2) • (f'' w) w<VAR>g' : ℝ → F := fun t => (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w<VAR>hg' : g' = fun t => (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w<VAR>g_deriv : ∀ t ∈ Icc 0 1, HasDerivWithinAt g (g' t) (Icc 0 1) t<VAR>g'_bound : ∀ t ∈ Ico 0 1, ‖g' t‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2<GOAL>‖f (x + h • v + h • w) - f (x + h • v) - h • (f' x) w - h ^ 2 • (f'' v) w - (h ^ 2 / 2) • (f'' w) w‖ ≤ ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * h ^ 2‖
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖<VAR>v w : E<VAR>hv : x + v ∈ interior s<VAR>hw : x + v + w ∈ interior s<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 => ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}<VAR>E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ<VAR>E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1<VAR>h : ℝ<VAR>hδ : h * (‖v‖ + ‖w‖) < δ<VAR>h_lt_1 : h < 1<VAR>hpos : 0 < h<VAR>xt_mem : ∀ t ∈ Icc 0 1, x + h • v + (t * h) • w ∈ interior s<VAR>g : ℝ → F := fun t => f (x + h • v + (t * h) • w) - (t * h) • (f' x) w - (t * h ^ 2) • (f'' v) w - ((t * h) ^ 2 / 2) • (f'' w) w<VAR>g' : ℝ → F := fun t => (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w<VAR>hg' : g' = fun t => (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w<VAR>g_deriv : ∀ t ∈ Icc 0 1, HasDerivWithinAt g (g' t) (Icc 0 1) t<VAR>g'_bound : ∀ t ∈ Ico 0 1, ‖g' t‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2<VAR>I : ‖g 1 - g 0‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2<GOAL>‖f (x + h • v + h • w) - f (x + h • v) - h • (f' x) w - h ^ 2 • (f'' v) w - (h ^ 2 / 2) • (f'' w) w‖ ≤ ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * h ^ 2‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : LinearOrderedField 𝕜<VAR>x y z : 𝕜<VAR>h : x ≤ y<GOAL>z ∈ Icc x y ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PartialOrder α<VAR>s : Set α<VAR>inst✝ : SeparableSpace ↑s<VAR>hs : Dense s<GOAL>∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PartialOrder α<VAR>s : Set α<VAR>inst✝ : SeparableSpace ↑s<VAR>hs : Dense s<VAR>t : Set α<VAR>hts : t ⊆ s<VAR>htc : t.Countable<VAR>htd : Dense t<GOAL>∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PartialOrder α<VAR>s : Set α<VAR>inst✝ : SeparableSpace ↑s<VAR>hs : Dense s<VAR>t : Set α<VAR>hts : t ⊆ s<VAR>htc : t.Countable<VAR>htd : Dense t<GOAL>(t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s ⊆ s
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PartialOrder α<VAR>s : Set α<VAR>inst✝ : SeparableSpace ↑s<VAR>hs : Dense s<VAR>t : Set α<VAR>hts : t ⊆ s<VAR>htc : t.Countable<VAR>htd : Dense t<GOAL>((t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s).Countable
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PartialOrder α<VAR>s : Set α<VAR>inst✝ : SeparableSpace ↑s<VAR>hs : Dense s<VAR>t : Set α<VAR>hts : t ⊆ s<VAR>htc : t.Countable<VAR>htd : Dense t<GOAL>Dense ((t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s)
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PartialOrder α<VAR>s : Set α<VAR>inst✝ : SeparableSpace ↑s<VAR>hs : Dense s<VAR>t : Set α<VAR>hts : t ⊆ s<VAR>htc : t.Countable<VAR>htd : Dense t<GOAL>∀ (x : α), IsBot x → x ∈ s → x ∈ (t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PartialOrder α<VAR>s : Set α<VAR>inst✝ : SeparableSpace ↑s<VAR>hs : Dense s<VAR>t : Set α<VAR>hts : t ⊆ s<VAR>htc : t.Countable<VAR>htd : Dense t<GOAL>∀ (x : α), IsTop x → x ∈ s → x ∈ (t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>f : Filter X<VAR>hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f<GOAL>sᶜ ∈ f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>f : Filter X<VAR>hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f<VAR>x : X<VAR>hx : x ∈ s<GOAL>sᶜ ∈ 𝓝 x ⊓ f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>hs : IsCompact s<VAR>f : Filter X<VAR>hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f<VAR>x : X<VAR>hx : x ∈ s<VAR>t : Set X<VAR>ht : t ∈ 𝓝[s] x<VAR>hst : tᶜ ∈ f<GOAL>sᶜ ∈ 𝓝 x ⊓ f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>hs : IsCompact s<VAR>f : Filter X<VAR>hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f<VAR>x : X<VAR>hx : x ∈ s<VAR>t : Set X<VAR>hst : tᶜ ∈ f<VAR>ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 x<GOAL>sᶜ ∈ 𝓝 x ⊓ f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>hs : IsCompact s<VAR>f : Filter X<VAR>hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f<VAR>x : X<VAR>hx : x ∈ s<VAR>t : Set X<VAR>hst : tᶜ ∈ f<VAR>ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 x<GOAL>{x | x ∈ s → x ∈ t} ∩ tᶜ ⊆ sᶜ
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : R<VAR>hb : b ≠ 0<VAR>A : ι → R<VAR>h : abv.IsAdmissible<GOAL>∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : R<VAR>hb : b ≠ 0<VAR>A : ι → R<VAR>h : abv.IsAdmissible<VAR>n : ℕ<VAR>e : ι ≃ Fin n<GOAL>∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : R<VAR>hb : b ≠ 0<VAR>A : ι → R<VAR>h : abv.IsAdmissible<VAR>n : ℕ<VAR>e : ι ≃ Fin n<VAR>t : Fin n → Fin (h.card ε)<VAR>ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv ((A ∘ ⇑e.symm) i₁ % b - (A ∘ ⇑e.symm) i₀ % b)) < abv b • ε<GOAL>∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : R<VAR>hb : b ≠ 0<VAR>A : ι → R<VAR>h✝ : abv.IsAdmissible<VAR>n : ℕ<VAR>e : ι ≃ Fin n<VAR>t : Fin n → Fin (h✝.card ε)<VAR>ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv ((A ∘ ⇑e.symm) i₁ % b - (A ∘ ⇑e.symm) i₀ % b)) < abv b • ε<VAR>i₀ i₁ : ι<VAR>h : (t ∘ ⇑e) i₀ = (t ∘ ⇑e) i₁<GOAL>↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>x : F.M<GOAL>M.mk x.dest = x
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>x : F.M<GOAL>∀ (i : ℕ), (M.mk x.dest).approx i = x.approx i
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>x : F.M<VAR>n : ℕ<VAR>a✝ : Approx.sMk x.dest n = x.approx n<VAR>hd : F.A<VAR>h' : hd = head' (x.approx 1)<VAR>ch : F.B (head' (x.approx 1)) → CofixA F n<VAR>h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch<VAR>a : F.B (head' (x.approx 1))<VAR>a'' : F.B (head' (x.approx n.succ))<VAR>hh : cast ⋯ a = a''<GOAL>children' (x.approx n.succ) a'' = ch a
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>x : F.M<VAR>n : ℕ<VAR>a✝ : Approx.sMk x.dest n = x.approx n<VAR>hd : F.A<VAR>h' : hd = head' (x.approx 1)<VAR>ch : F.B (head' (x.approx 1)) → CofixA F n<VAR>h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch<VAR>a : F.B (head' (x.approx 1))<VAR>a'' : F.B (head' (x.approx n.succ))<VAR>hh : HEq a a''<GOAL>children' (x.approx n.succ) a'' = ch a