ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.OuterRegular<VAR>hp : p ≠ ⊤<VAR>s u : Set α<VAR>s_closed : IsClosed s<VAR>u_open : IsOpen u<VAR>hsu : s ⊆ u<VAR>hs : μ s ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>η : ℝ≥0<VAR>η_pos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ ε<VAR>ηpos : 0 < ↑η<VAR>V : Set α<VAR>sV : V ⊇ s<VAR>V_open : IsOpen V<VAR>h'V : μ V < ⊤<VAR>hV : μ (V \ s) < ↑η<VAR>v : Set α := u ∩ V<VAR>hsv : s ⊆ v<VAR>hμv : μ v < ⊤<VAR>g : C(α, ℝ)<VAR>hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ<VAR>hgs : EqOn (⇑g) 1 s<VAR>hg_range : ∀ (x : α), g x ∈ Icc 0 1<VAR>g_norm : ∀ (x : α), ‖g x‖ = g x<VAR>gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖<GOAL>∃ f, Continuous f ∧ eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.OuterRegular<VAR>hp : p ≠ ⊤<VAR>s u : Set α<VAR>s_closed : IsClosed s<VAR>u_open : IsOpen u<VAR>hsu : s ⊆ u<VAR>hs : μ s ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>η : ℝ≥0<VAR>η_pos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ ε<VAR>ηpos : 0 < ↑η<VAR>V : Set α<VAR>sV : V ⊇ s<VAR>V_open : IsOpen V<VAR>h'V : μ V < ⊤<VAR>hV : μ (V \ s) < ↑η<VAR>v : Set α := u ∩ V<VAR>hsv : s ⊆ v<VAR>hμv : μ v < ⊤<VAR>g : C(α, ℝ)<VAR>hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ<VAR>hgs : EqOn (⇑g) 1 s<VAR>hg_range : ∀ (x : α), g x ∈ Icc 0 1<VAR>g_norm : ∀ (x : α), ‖g x‖ = g x<VAR>gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖<VAR>gc_bd : ∀ (x : α), ‖g x • c - s.indicator (fun _x => c) x‖ ≤ ‖(v \ s).indicator (fun _x => c) x‖<GOAL>∃ f, Continuous f ∧ eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.OuterRegular<VAR>hp : p ≠ ⊤<VAR>s u : Set α<VAR>s_closed : IsClosed s<VAR>u_open : IsOpen u<VAR>hsu : s ⊆ u<VAR>hs : μ s ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>η : ℝ≥0<VAR>η_pos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ ε<VAR>ηpos : 0 < ↑η<VAR>V : Set α<VAR>sV : V ⊇ s<VAR>V_open : IsOpen V<VAR>h'V : μ V < ⊤<VAR>hV : μ (V \ s) < ↑η<VAR>v : Set α := u ∩ V<VAR>hsv : s ⊆ v<VAR>hμv : μ v < ⊤<VAR>g : C(α, ℝ)<VAR>hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ<VAR>hgs : EqOn (⇑g) 1 s<VAR>hg_range : ∀ (x : α), g x ∈ Icc 0 1<VAR>g_norm : ∀ (x : α), ‖g x‖ = g x<VAR>gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖<VAR>gc_bd : ∀ (x : α), ‖g x • c - s.indicator (fun _x => c) x‖ ≤ ‖(v \ s).indicator (fun _x => c) x‖<VAR>gc_support : (Function.support fun x => g x • c) ⊆ v<GOAL>∃ f, Continuous f ∧ eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.OuterRegular<VAR>hp : p ≠ ⊤<VAR>s u : Set α<VAR>s_closed : IsClosed s<VAR>u_open : IsOpen u<VAR>hsu : s ⊆ u<VAR>hs : μ s ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>η : ℝ≥0<VAR>η_pos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ ε<VAR>ηpos : 0 < ↑η<VAR>V : Set α<VAR>sV : V ⊇ s<VAR>V_open : IsOpen V<VAR>h'V : μ V < ⊤<VAR>hV : μ (V \ s) < ↑η<VAR>v : Set α := u ∩ V<VAR>hsv : s ⊆ v<VAR>hμv : μ v < ⊤<VAR>g : C(α, ℝ)<VAR>hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ<VAR>hgs : EqOn (⇑g) 1 s<VAR>hg_range : ∀ (x : α), g x ∈ Icc 0 1<VAR>g_norm : ∀ (x : α), ‖g x‖ = g x<VAR>gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖<VAR>gc_bd : ∀ (x : α), ‖g x • c - s.indicator (fun _x => c) x‖ ≤ ‖(v \ s).indicator (fun _x => c) x‖<VAR>gc_support : (Function.support fun x => g x • c) ⊆ v<VAR>gc_mem : Memℒp (fun x => g x • c) p μ<GOAL>∃ f, Continuous f ∧ eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.OuterRegular<VAR>hp : p ≠ ⊤<VAR>s u : Set α<VAR>s_closed : IsClosed s<VAR>u_open : IsOpen u<VAR>hsu : s ⊆ u<VAR>hs : μ s ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>η : ℝ≥0<VAR>η_pos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ ε<VAR>ηpos : 0 < ↑η<VAR>V : Set α<VAR>sV : V ⊇ s<VAR>V_open : IsOpen V<VAR>h'V : μ V < ⊤<VAR>hV : μ (V \ s) < ↑η<VAR>v : Set α := u ∩ V<VAR>hsv : s ⊆ v<VAR>hμv : μ v < ⊤<VAR>g : C(α, ℝ)<VAR>hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ<VAR>hgs : EqOn (⇑g) 1 s<VAR>hg_range : ∀ (x : α), g x ∈ Icc 0 1<VAR>g_norm : ∀ (x : α), ‖g x‖ = g x<VAR>gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖<VAR>gc_bd : ∀ (x : α), ‖g x • c - s.indicator (fun _x => c) x‖ ≤ ‖(v \ s).indicator (fun _x => c) x‖<VAR>gc_support : (Function.support fun x => g x • c) ⊆ v<VAR>gc_mem : Memℒp (fun x => g x • c) p μ<GOAL>eLpNorm ((v \ s).indicator fun _x => c) p μ ≤ ε
<VAR>p : ℝ<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<GOAL>StrictConcaveOn ℝ≥0 univ fun x => x ^ p
<VAR>p : ℝ<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<VAR>hp₀' : 0 < 1 / p<GOAL>StrictConcaveOn ℝ≥0 univ fun x => x ^ p
<VAR>p : ℝ<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<VAR>hp₀' : 0 < 1 / p<VAR>hp₁' : 1 < 1 / p<GOAL>StrictConcaveOn ℝ≥0 univ fun x => x ^ p
<VAR>p : ℝ<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<VAR>hp₀' : 0 < 1 / p<VAR>hp₁' : 1 < 1 / p<VAR>f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'<GOAL>StrictConcaveOn ℝ≥0 univ fun x => x ^ p
<VAR>p : ℝ<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<VAR>hp₀' : 0 < 1 / p<VAR>hp₁' : 1 < 1 / p<VAR>f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'<VAR>h₁ : StrictConvexOn ℝ≥0 univ ⇑f<GOAL>StrictConcaveOn ℝ≥0 univ fun x => x ^ p
<VAR>p : ℝ<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<VAR>hp₀' : 0 < 1 / p<VAR>hp₁' : 1 < 1 / p<VAR>f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'<VAR>h₁ : StrictConvexOn ℝ≥0 univ ⇑f<VAR>h₂ : ∀ (x : ℝ≥0), f.symm x = x ^ p<GOAL>StrictConcaveOn ℝ≥0 univ fun x => x ^ p
<VAR>p : ℝ<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<VAR>hp₀' : 0 < 1 / p<VAR>hp₁' : 1 < 1 / p<VAR>f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'<VAR>h₁ : StrictConvexOn ℝ≥0 univ ⇑f<VAR>h₂ : ∀ (x : ℝ≥0), f.symm x = x ^ p<VAR>x : ℝ≥0<VAR>mx : x ∈ univ<VAR>y : ℝ≥0<VAR>my : y ∈ univ<VAR>hxy : x ≠ y<VAR>a b : ℝ≥0<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
<VAR>p : ℝ<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<VAR>hp₀' : 0 < 1 / p<VAR>hp₁' : 1 < 1 / p<VAR>f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'<VAR>h₁ : StrictConvexOn ℝ≥0 univ ⇑f<VAR>h₂ : ∀ (x : ℝ≥0), f.symm x = x ^ p<VAR>x : ℝ≥0<VAR>mx : x ∈ univ<VAR>y : ℝ≥0<VAR>my : y ∈ univ<VAR>hxy : x ≠ y<VAR>a b : ℝ≥0<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • f.symm x + b • f.symm y < f.symm (a • x + b • y)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<VAR>i : ι<GOAL>b.repr ((fun i => b.repr.symm (lp.single 2 i 1)) i) = lp.single 2 i 1
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝¹ : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)<VAR>i j : J<VAR>f : i ⟶ j<VAR>X : Cᵒᵖ<GOAL>Hom.app (F.map f ≫ colimitCoconeιApp F j) X = Hom.app (colimitCoconeιApp F i) X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s : Set α<VAR>t : Set β<VAR>x✝ : α × β<GOAL>x✝ ∈ ↑(upperClosure (s ×ˢ t)) ↔ x✝ ∈ ↑(upperClosure s ×ˢ upperClosure t)
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>(ndinsert a s).gcd = GCDMonoid.gcd a s.gcd
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<GOAL>IH24 x₁ x₂ y → IH24 (-x₂) (-x₁) y ∧ IH24 x₁ x₂ (-y)
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<GOAL>(∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)) → (∀ ⦃z : PGame⦄, ((-z).IsOption x₂ → P24 z (-x₁) y) ∧ ((-z).IsOption x₁ → P24 (-x₂) z y) ∧ (z.IsOption y → P24 (-x₂) (-x₁) z)) ∧ ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ ((-z).IsOption y → P24 x₁ x₂ z)
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)<VAR>z : PGame<GOAL>(-z).IsOption x₂ → P24 z (-x₁) y
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)<VAR>z : PGame<GOAL>(-z).IsOption x₁ → P24 (-x₂) z y
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)<VAR>z : PGame<GOAL>z.IsOption y → P24 (-x₂) (-x₁) z
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>x y : α<VAR>inst✝¹ : LT α<VAR>inst✝ : LTCmp cmp<GOAL>cmp x y = Ordering.gt ↔ y < x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NormedCommRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<GOAL>B.polar {0} = Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NormedCommRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>y : F<VAR>x : E<VAR>hx : x ∈ {0}<GOAL>‖(B x) y‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NormedCommRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>y : F<VAR>x : E<VAR>hx : x ∈ {0}<GOAL>0 ≤ 1
<VAR>J K : Type v<VAR>inst✝⁵ : SmallCategory J<VAR>inst✝⁴ : SmallCategory K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>inst✝² : HasColimitsOfShape K C<VAR>inst✝¹ : HasColimit (uncurry.obj F)<VAR>inst✝ : HasColimit (F ⋙ colim)<VAR>j : J<VAR>k : K<GOAL>colimit.ι (uncurry.obj F) (j, k) ≫ (colimitUncurryIsoColimitCompColim F).hom = colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j
<VAR>J K : Type v<VAR>inst✝⁵ : SmallCategory J<VAR>inst✝⁴ : SmallCategory K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>inst✝² : HasColimitsOfShape K C<VAR>inst✝¹ : HasColimit (uncurry.obj F)<VAR>inst✝ : HasColimit (F ⋙ colim)<VAR>j : J<VAR>k : K<GOAL>(colimit.ι (uncurry.obj F) (j, k) ≫ (colimitUncurryIsoColimitCompColim F).hom) ≫ (colimitUncurryIsoColimitCompColim F).inv = (colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j) ≫ (colimitUncurryIsoColimitCompColim F).inv
<VAR>ι : Type u_1<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : Group α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : GroupSeminormClass F α β<VAR>f : F<VAR>x y : α<GOAL>f (x / y) = f (y / x)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<GOAL>ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<GOAL>ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<GOAL>ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<VAR>hVo : IsOpen V<GOAL>ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<VAR>hVo : IsOpen V<GOAL>ContinuousOn (fun p => jacobiTheta₂' p.1 p.2) V
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<VAR>hVo : IsOpen V<VAR>u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))<GOAL>ContinuousOn (fun p => jacobiTheta₂' p.1 p.2) V
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<VAR>hVo : IsOpen V<VAR>u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))<VAR>hu : Summable u<GOAL>ContinuousOn (fun p => jacobiTheta₂' p.1 p.2) V
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<VAR>hVo : IsOpen V<VAR>u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))<VAR>hu : Summable u<VAR>n : ℤ<GOAL>ContinuousOn (fun p => jacobiTheta₂'_term n p.1 p.2) V
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ'✝ : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<VAR>hVo : IsOpen V<VAR>u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))<VAR>hu : Summable u<VAR>n : ℤ<VAR>x✝¹ : ℂ × ℂ<VAR>z' τ' : ℂ<VAR>x✝ : (z', τ') ∈ V<VAR>hz' : (z', τ').1 ∈ {u | |u.im| < S}<VAR>hτ' : (z', τ').2 ∈ {v | T < v.im}<GOAL>‖jacobiTheta₂'_term n (z', τ').1 (z', τ').2‖ ≤ u n
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsBezout R<VAR>inst✝ : GCDMonoid R<VAR>a b z : R<GOAL>gcd a b ∣ z ↔ ∃ x y, z = a * x + b * y
<VAR>K : Type u_1<VAR>inst✝ : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>M : Λ → Stmt₂<VAR>S : Finset Λ<VAR>q₁ q₂ : Stmt₂<VAR>h₁ : q₁ ∈ stmts₁ q₂<GOAL>some q₂ ∈ stmts M S → some q₁ ∈ stmts M S
<VAR>K : Type u_1<VAR>inst✝ : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>M : Λ → Stmt₂<VAR>S : Finset Λ<VAR>q₁ q₂ : Stmt₂<VAR>h₁ : q₁ ∈ stmts₁ q₂<GOAL>∀ x ∈ S, q₂ ∈ stmts₁ (M x) → ∃ a ∈ S, q₁ ∈ stmts₁ (M a)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hfi : Integrable f μ<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ∃ t, MeasurableSet t ∧ μ t ≠ 0 ∧ μ tᶜ ≠ 0 ∧ ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hfi : Integrable f μ<VAR>H : ¬∃ t, MeasurableSet t ∧ μ t ≠ 0 ∧ μ tᶜ ≠ 0 ∧ ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hfi : Integrable f μ<VAR>H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t✝ : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hfi : Integrable f μ<VAR>H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>ht' : μ t < ⊤<GOAL>∫ (x : α) in t, f x ∂μ = ∫ (x : α) in t, const α (⨍ (x : α), f x ∂μ) x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t✝ : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hfi : Integrable f μ<VAR>H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>∫ (x : α) in t, f x ∂μ = ∫ (x : α) in t, const α (⨍ (x : α), f x ∂μ) x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t✝ : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hfi : Integrable f μ<VAR>H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>∫ (x : α) in t, f x ∂μ = (μ t).toReal • ⨍ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t✝ : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hfi : Integrable f μ<VAR>H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>h₀ : ¬μ t = 0<VAR>h₀' : ¬μ tᶜ = 0<GOAL>∫ (x : α) in t, f x ∂μ = (μ t).toReal • ⨍ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t✝ : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hfi : Integrable f μ<VAR>H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>h₀ : ¬μ t = 0<VAR>h₀' : ¬μ tᶜ = 0<VAR>this : ⨍ (x : α), f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)<GOAL>∫ (x : α) in t, f x ∂μ = (μ t).toReal • ⨍ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t✝ : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hfi : Integrable f μ<VAR>H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>h₀ : ¬μ t = 0<VAR>h₀' : ¬μ tᶜ = 0<VAR>this : ⨍ (x : α), f x ∂μ = ⨍ (x : α) in t, f x ∂μ<GOAL>∫ (x : α) in t, f x ∂μ = (μ t).toReal • ⨍ (x : α), f x ∂μ
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : Nonempty ι<VAR>P : Type u₁<VAR>inst✝ : L.Structure P<VAR>g : (i : ι) → G i ↪[L] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<GOAL>(lift L ι G f g Hg).toHom.range = ⨆ i, (g i).toHom.range
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : Nonempty ι<VAR>P : Type u₁<VAR>inst✝ : L.Structure P<VAR>g : (i : ι) → G i ↪[L] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<GOAL>Substructure.map (lift L ι G f g Hg).toHom ⊤ = ⨆ i, Substructure.map (g i).toHom ⊤
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : Nonempty ι<VAR>P : Type u₁<VAR>inst✝ : L.Structure P<VAR>g : (i : ι) → G i ↪[L] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<GOAL>⨆ i, Substructure.map (lift L ι G f g Hg).toHom (of L ι G f i).toHom.range = ⨆ i, Substructure.map (g i).toHom ⊤
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : Nonempty ι<VAR>P : Type u₁<VAR>inst✝ : L.Structure P<VAR>g : (i : ι) → G i ↪[L] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<GOAL>⨆ i, Substructure.map ((lift L ι G f g Hg).toHom.comp (of L ι G f i).toHom) ⊤ = ⨆ i, Substructure.map (g i).toHom ⊤
<VAR>z : ℤ<VAR>hz : normalize z = z<GOAL>|z| = z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>b : M<VAR>i : α<VAR>inst✝ : DecidableEq α<VAR>h : b ≠ 0<GOAL>(f.update a b).support = insert a f.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>a : αˣ<VAR>hp : p ≠ 0<VAR>x : α<VAR>hx : ¬IsUnit x<VAR>hx' : p * ↑a = p * x<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>a : αˣ<VAR>hp : p ≠ 0<VAR>hx : ¬IsUnit ↑a<VAR>hx' : p * ↑a = p * ↑a<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<VAR>t : Set α<GOAL>t ∈ l ⊔ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∪ s' i.snd ⊆ t