ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>SecondCountableTopology α<GOAL>Measurable fun p => nndist p.1 p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>SecondCountableTopology α<VAR>f g : β → α<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun b => nndist (f b) (g b)
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>x : α<VAR>ε : ℝ≥0∞<GOAL>MeasurableSet (EMetric.ball x ε)
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>x : α<GOAL>Measurable (edist x)
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>x : α<GOAL>Measurable fun y => edist y x
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>s : Set α<GOAL>Measurable fun x => EMetric.infEdist x s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<VAR>s : Set α<GOAL>Measurable fun x => EMetric.infEdist (f x) s
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : ∃ R > 0, μ (Metric.cthickening R s) ≠ ⊤<GOAL>Filter.Tendsto (fun r => μ (Metric.cthickening r s)) (𝓝 0) (𝓝 (μ (closure s)))
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : ∃ R > 0, μ (Metric.cthickening R s) ≠ ⊤<VAR>h's : IsClosed s<GOAL>Filter.Tendsto (fun r => μ (Metric.cthickening r s)) (𝓝 0) (𝓝 (μ s))
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : ∃ R > 0, μ (Metric.thickening R s) ≠ ⊤<GOAL>Filter.Tendsto (fun r => μ (Metric.thickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : ∃ R > 0, μ (Metric.thickening R s) ≠ ⊤<VAR>h's : IsClosed s<GOAL>Filter.Tendsto (fun r => μ (Metric.thickening r s)) (𝓝[>] 0) (𝓝 (μ s))
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>SecondCountableTopology α<GOAL>Measurable fun p => edist p.1 p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>SecondCountableTopology α<VAR>f g : β → α<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun b => edist (f b) (g b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>SecondCountableTopology α<VAR>f g : β → α<VAR>μ : MeasureTheory.Measure β<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun a => edist (f a) (g a)) μ
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>ProperSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>s : Set α<VAR>hs : IsCompact s<GOAL>Filter.Tendsto (fun r => μ (Metric.cthickening r s)) (𝓝 0) (𝓝 (μ s))
<VAR>α : Type u_5<VAR>m : MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<VAR>MeasurableSpace.SeparatesPoints α<GOAL>∃ τ, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α
<VAR>α : Type u_5<VAR>m : MeasurableSpace α<VAR>MeasurableSpace.CountablySeparated α<GOAL>∃ τ, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>NormedAddCommGroup α<VAR>OpensMeasurableSpace α<GOAL>Measurable norm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>NormedAddCommGroup α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<GOAL>Measurable fun a => ‖f a‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>NormedAddCommGroup α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>μ : MeasureTheory.Measure β<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun a => ‖f a‖) μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>NormedAddCommGroup α<VAR>OpensMeasurableSpace α<GOAL>Measurable nnnorm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>NormedAddCommGroup α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<GOAL>Measurable fun a => ‖f a‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>NormedAddCommGroup α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>μ : MeasureTheory.Measure β<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun a => ‖f a‖₊) μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>NormedAddCommGroup α<VAR>OpensMeasurableSpace α<GOAL>Measurable fun x => ↑‖x‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>NormedAddCommGroup α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<GOAL>Measurable fun a => ↑‖f a‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>NormedAddCommGroup α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>μ : MeasureTheory.Measure β<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun a => ↑‖f a‖₊) μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>s : Set ↑(Metric.sphere 0 1)<VAR>r : ↑(Set.Ioi 0)<GOAL>μ (Subtype.val '' (⇑(homeomorphUnitSphereProd E) ⁻¹' s ×ˢ Set.Iio r)) = μ (Set.Ioo 0 ↑r • Subtype.val '' s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>s : Set ↑(Metric.sphere 0 1)<VAR>hs : MeasurableSet s<GOAL>μ.toSphere s = ↑(dim E) * μ (Set.Ioo 0 1 • Subtype.val '' s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<GOAL>μ.toSphere Set.univ = ↑(dim E) * μ (Metric.ball 0 1 \ {0})
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<GOAL>μ.toSphere Set.univ = ↑(dim E) * μ (Metric.ball 0 1)
<VAR>n : ℕ<VAR>x : ↑(Set.Ioi 0)<GOAL>(MeasureTheory.Measure.volumeIoiPow n) (Set.Iio x) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<GOAL>MeasureTheory.MeasurePreserving (⇑(homeomorphUnitSphereProd E)) (MeasureTheory.Measure.comap Subtype.val μ) (μ.toSphere.prod (MeasureTheory.Measure.volumeIoiPow (dim E - 1)))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>Nontrivial E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>f : ℝ → F<GOAL>∫ (x : E), f ‖x‖ ∂μ = dim E • (μ (Metric.ball 0 1)).toReal • ∫ (y : ℝ) in Set.Ioi 0, y ^ (dim E - 1) • f y
<VAR>c : ℂ<VAR>R : ℝ<GOAL>Function.Periodic (circleMap c R) (2 * π)
<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>c : ℂ<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>(circleMap c R ⁻¹' s).Countable
<VAR>c : ℂ<VAR>R θ : ℝ<GOAL>circleMap c R θ - c = circleMap 0 R θ
<VAR>R θ : ℝ<GOAL>circleMap 0 R θ = ↑R * cexp (↑θ * Complex.I)
<VAR>R θ : ℝ<GOAL>Complex.abs (circleMap 0 R θ) = |R|
<VAR>c : ℂ<VAR>R θ : ℝ<GOAL>circleMap c R θ ∈ Metric.sphere c |R|
<VAR>c : ℂ<VAR>R : ℝ<VAR>hR : 0 ≤ R<VAR>θ : ℝ<GOAL>circleMap c R θ ∈ Metric.sphere c R
<VAR>c : ℂ<VAR>R : ℝ<VAR>hR : 0 ≤ R<VAR>θ : ℝ<GOAL>circleMap c R θ ∈ Metric.closedBall c R
<VAR>c : ℂ<VAR>R θ : ℝ<GOAL>circleMap c R θ ∉ Metric.ball c R
<VAR>c : ℂ<VAR>R : ℝ<VAR>w : ℂ<VAR>hw : w ∈ Metric.ball c R<VAR>θ : ℝ<GOAL>circleMap c R θ ≠ w
<VAR>c : ℂ<VAR>R : ℝ<GOAL>Set.range (circleMap c R) = Metric.sphere c |R|
<VAR>c : ℂ<VAR>R : ℝ<GOAL>circleMap c R '' Set.Ioc 0 (2 * π) = Metric.sphere c |R|
<VAR>c : ℂ<VAR>R θ : ℝ<GOAL>circleMap c R θ = c ↔ R = 0
<VAR>c : ℂ<GOAL>circleMap c 0 = Function.const ℝ c
<VAR>c : ℂ<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>θ : ℝ<GOAL>circleMap c R θ ≠ c
<VAR>c : ℂ<VAR>R θ : ℝ<GOAL>HasDerivAt (circleMap c R) (circleMap 0 R θ * Complex.I) θ
<VAR>c : ℂ<VAR>R : ℝ<GOAL>Differentiable ℝ (circleMap c R)
<VAR>c : ℂ<VAR>R : ℝ<GOAL>Continuous (circleMap c R)
<VAR>c : ℂ<VAR>R : ℝ<GOAL>Measurable (circleMap c R)
<VAR>c : ℂ<VAR>R θ : ℝ<GOAL>deriv (circleMap c R) θ = circleMap 0 R θ * Complex.I
<VAR>c : ℂ<VAR>R θ : ℝ<GOAL>deriv (circleMap c R) θ = 0 ↔ R = 0
<VAR>c : ℂ<VAR>R θ : ℝ<VAR>hR : R ≠ 0<GOAL>deriv (circleMap c R) θ ≠ 0
<VAR>c : ℂ<VAR>R : ℝ<GOAL>LipschitzWith (Real.nnabs R) (circleMap c R)
<VAR>R : ℝ<VAR>z w : ℂ<VAR>hw : w ∈ Metric.ball z R<GOAL>Continuous fun θ => (circleMap z R θ - w)⁻¹
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>a : E<VAR>c : ℂ<VAR>R : ℝ<GOAL>CircleIntegrable (fun x => a) c R
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f g : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>hf : CircleIntegrable f c R<VAR>hg : CircleIntegrable g c R<GOAL>CircleIntegrable (f + g) c R
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>hf : CircleIntegrable f c R<GOAL>CircleIntegrable (-f) c R
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>NormedSpace ℂ E<VAR>hf : CircleIntegrable f c R<GOAL>IntervalIntegrable (fun θ => deriv (circleMap c R) θ • f (circleMap c R θ)) MeasureTheory.volume 0 (2 * π)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℂ → E<VAR>c : ℂ<GOAL>CircleIntegrable f c 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<GOAL>CircleIntegrable f c R ↔ IntervalIntegrable (fun θ => deriv (circleMap c R) θ • f (circleMap c R θ)) MeasureTheory.volume 0 (2 * π)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>hf : ContinuousOn f (Metric.sphere c |R|)<GOAL>CircleIntegrable f c R
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>hR : 0 ≤ R<VAR>hf : ContinuousOn f (Metric.sphere c R)<GOAL>CircleIntegrable f c R
<VAR>c w : ℂ<VAR>R : ℝ<VAR>n : ℤ<GOAL>CircleIntegrable (fun z => (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ w ∉ Metric.sphere c |R|
<VAR>c w : ℂ<VAR>R : ℝ<GOAL>CircleIntegrable (fun z => (z - w)⁻¹) c R ↔ R = 0 ∨ w ∉ Metric.sphere c |R|
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<GOAL>(∮ (z : ℂ) in C(c, R), f z) = ∫ (θ : ℝ) in Set.Icc 0 (2 * π), deriv (circleMap c R) θ • f (circleMap c R θ)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<GOAL>(∮ (z : ℂ) in C(c, 0), f z) = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>hR : 0 ≤ R<VAR>h : Set.EqOn f g (Metric.sphere c R)<GOAL>(∮ (z : ℂ) in C(c, R), f z) = ∮ (z : ℂ) in C(c, R), g z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c w : ℂ<VAR>R : ℝ<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, R), f z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>hf : ¬CircleIntegrable f c R<GOAL>(∮ (z : ℂ) in C(c, R), f z) = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>hf : CircleIntegrable f c R<VAR>hg : CircleIntegrable g c R<GOAL>(∮ (z : ℂ) in C(c, R), f z - g z) = (∮ (z : ℂ) in C(c, R), f z) - ∮ (z : ℂ) in C(c, R), g z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R C : ℝ<VAR>hf : ∀ z ∈ Metric.sphere c |R|, ‖f z‖ ≤ C<GOAL>‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * π * |R| * C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R C : ℝ<VAR>hR : 0 ≤ R<VAR>hf : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C<GOAL>‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * π * R * C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R C : ℝ<VAR>hR : 0 ≤ R<VAR>hf : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C<GOAL>‖(2 * ↑π * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), f z‖ ≤ R * C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R C : ℝ<VAR>hR : 0 < R<VAR>hc : ContinuousOn f (Metric.sphere c R)<VAR>hf : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C<VAR>hlt : ∃ z ∈ Metric.sphere c R, ‖f z‖ < C<GOAL>‖∮ (z : ℂ) in C(c, R), f z‖ < 2 * π * R * C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>SMulCommClass 𝕜 ℂ E<VAR>a : 𝕜<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<GOAL>(∮ (z : ℂ) in C(c, R), a • f z) = a • ∮ (z : ℂ) in C(c, R), f z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → ℂ<VAR>a : E<VAR>c : ℂ<VAR>R : ℝ<GOAL>(∮ (z : ℂ) in C(c, R), f z • a) = (∮ (z : ℂ) in C(c, R), f z) • a
<VAR>a : ℂ<VAR>f : ℂ → ℂ<VAR>c : ℂ<VAR>R : ℝ<GOAL>(∮ (z : ℂ) in C(c, R), a * f z) = a * ∮ (z : ℂ) in C(c, R), f z
<VAR>c : ℂ<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>(∮ (z : ℂ) in C(c, R), (z - c)⁻¹) = 2 * ↑π * Complex.I
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f f' : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>h : ∀ z ∈ Metric.sphere c |R|, HasDerivWithinAt f (f' z) (Metric.sphere c |R|) z<GOAL>(∮ (z : ℂ) in C(c, R), f' z) = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f f' : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>hR : 0 ≤ R<VAR>h : ∀ z ∈ Metric.sphere c R, HasDerivWithinAt f (f' z) (Metric.sphere c R) z<GOAL>(∮ (z : ℂ) in C(c, R), f' z) = 0
<VAR>n : ℤ<VAR>c w : ℂ<VAR>R : ℝ<VAR>hn : n < 0<VAR>hw : w ∈ Metric.sphere c |R|<GOAL>(∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
<VAR>n : ℤ<VAR>hn : n ≠ -1<VAR>c w : ℂ<VAR>R : ℝ<GOAL>(∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>n : ℕ<VAR>w : ℂ<GOAL>((cauchyPowerSeries f c R n) fun x => w) = (2 * ↑π * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>n : ℕ<GOAL>‖cauchyPowerSeries f c R n‖ ≤ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ≥0<GOAL>↑R ≤ (cauchyPowerSeries f c ↑R).radius
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>w : ℂ<VAR>hf : CircleIntegrable f c R<VAR>hw : Complex.abs w < R<GOAL>HasSum (fun n => ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>w : ℂ<VAR>hf : CircleIntegrable f c R<VAR>hw : Complex.abs w < R<GOAL>HasSum (fun n => (cauchyPowerSeries f c R n) fun x => w) ((2 * ↑π * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>w : ℂ<VAR>hf : CircleIntegrable f c R<VAR>hw : Complex.abs w < R<GOAL>(cauchyPowerSeries f c R).sum w = (2 * ↑π * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ≥0<VAR>hf : CircleIntegrable f c ↑R<VAR>hR : 0 < R<GOAL>HasFPowerSeriesOnBall (fun w => (2 * ↑π * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z) (cauchyPowerSeries f c ↑R) c ↑R
<VAR>c w : ℂ<VAR>R : ℝ<VAR>hw : w ∈ Metric.ball c R<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * Complex.I
<VAR>α : Type u_1<GOAL>Antitone (@borel α)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>DiscreteTopology α<GOAL>borel α = ⊤
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>T1Space α<VAR>Countable α<GOAL>borel α = ⊤
<VAR>α : Type u_1<VAR>s : Set (Set α)<VAR>t : TopologicalSpace α<VAR>SecondCountableTopology α<VAR>hs : t = TopologicalSpace.generateFrom s<GOAL>borel α = MeasurableSpace.generateFrom s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>s : Set (Set α)<VAR>hs : TopologicalSpace.IsTopologicalBasis s<GOAL>borel α = MeasurableSpace.generateFrom s
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>IsPiSystem {s | IsOpen s}
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>IsPiSystem {s | IsClosed s}
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>borel α = MeasurableSpace.generateFrom {s | IsClosed s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>t : TopologicalSpace β<GOAL>borel α = MeasurableSpace.comap f (borel β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : Continuous f<GOAL>Measurable f
<VAR>α : Type u_6<VAR>TopologicalSpace α<VAR>h : MeasurableSpace α<VAR>self : OpensMeasurableSpace α<GOAL>borel α ≤ h
<VAR>α : Type u_6<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>self : BorelSpace α<GOAL>inst✝ = borel α
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<GOAL>OpensMeasurableSpace α ↔ ∀ (s : Set α), IsOpen s → MeasurableSet s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>C : Set α → Prop<VAR>h_open : ∀ (U : Set α), IsOpen U → C U<VAR>h_compl : ∀ (t : Set α), MeasurableSet t → C t → C tᶜ<VAR>h_union : ∀ (f : ℕ → Set α), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ i, f i)<VAR>t : Set α<GOAL>MeasurableSet t → C t
<VAR>α : Type u_1<VAR>s : Set α<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>h : IsOpen s<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>s : Set α<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>h : IsOpen s<GOAL>MeasureTheory.NullMeasurableSet s μ
<VAR>α : Type u_1<VAR>s : Set α<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<GOAL>MeasurableSet (interior s)
<VAR>α : Type u_1<VAR>s : Set α<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>h : IsGδ s<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>β : Type u_6<VAR>EMetricSpace β<VAR>f : α → β<GOAL>MeasurableSet {x | ContinuousAt f x}
<VAR>α : Type u_1<VAR>s : Set α<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>h : IsClosed s<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>s : Set α<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>h : IsClosed s<GOAL>MeasureTheory.NullMeasurableSet s μ
<VAR>α : Type u_1<VAR>s : Set α<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>T2Space α<VAR>h : IsCompact s<GOAL>MeasurableSet s
<VAR>γ : Type u_3<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>x y : γ<VAR>h : Inseparable x y<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>x ∈ s ↔ y ∈ s
<VAR>γ : Type u_3<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>R1Space γ<VAR>K s : Set γ<VAR>hK : IsCompact K<VAR>hs : MeasurableSet s<VAR>hKs : K ⊆ s<GOAL>closure K ⊆ s
<VAR>γ : Type u_3<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>R1Space γ<VAR>K : Set γ<VAR>hK : IsCompact K<VAR>μ : MeasureTheory.Measure γ<GOAL>μ (closure K) = μ K
<VAR>α : Type u_1<VAR>s : Set α<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<GOAL>MeasurableSet (closure s)
<VAR>γ : Type u_3<VAR>δ : Type u_5<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>MeasurableSpace δ<VAR>f : δ → γ<VAR>hf : ∀ (s : Set γ), IsOpen s → MeasurableSet (f ⁻¹' s)<GOAL>Measurable f
<VAR>γ : Type u_3<VAR>δ : Type u_5<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>MeasurableSpace δ<VAR>f : δ → γ<VAR>hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)<GOAL>Measurable f
<VAR>γ : Type u_3<VAR>δ : Type u_5<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>MeasurableSpace δ<VAR>f : δ → γ<VAR>hf : ∀ (s : Set γ), IsClosed s → s.Nonempty → s ≠ Set.univ → MeasurableSet (f ⁻¹' s)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a : α<GOAL>(𝓝[s] a).IsMeasurablyGenerated
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>self : SecondCountableTopologyEither α β<GOAL>SecondCountableTopology α ∨ SecondCountableTopology β
<VAR>α' : Type u_6<VAR>TopologicalSpace α'<VAR>MeasurableSpace α'<VAR>μ : MeasureTheory.Measure α'<VAR>s : Set α'<VAR>h : μ (frontier s) = 0<GOAL>interior s =ᵐ[μ] s
<VAR>α' : Type u_6<VAR>TopologicalSpace α'<VAR>MeasurableSpace α'<VAR>μ : MeasureTheory.Measure α'<VAR>s : Set α'<VAR>h : μ (frontier s) = 0<GOAL>μ (interior s) = μ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : μ (frontier s) = 0<GOAL>MeasureTheory.NullMeasurableSet s μ
<VAR>α' : Type u_6<VAR>TopologicalSpace α'<VAR>MeasurableSpace α'<VAR>μ : MeasureTheory.Measure α'<VAR>s : Set α'<VAR>h : μ (frontier s) = 0<GOAL>closure s =ᵐ[μ] s
<VAR>α' : Type u_6<VAR>TopologicalSpace α'<VAR>MeasurableSpace α'<VAR>μ : MeasureTheory.Measure α'<VAR>s : Set α'<VAR>h : μ (frontier s) = 0<GOAL>μ (closure s) = μ s
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>f : α → γ<VAR>hf : Continuous f<GOAL>Measurable f
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>f : α → γ<VAR>h : Continuous f<VAR>μ : MeasureTheory.Measure α<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>f : α → γ<VAR>hf : ClosedEmbedding f<GOAL>Measurable f
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>f g : α → γ<VAR>s : Set α<VAR>(j : α) → Decidable (j ∈ s)<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g sᶜ<VAR>hs : MeasurableSet s<GOAL>Measurable (s.piecewise f g)
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>h : α ≃ₜ γ<GOAL>Measurable ⇑h
<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>TopologicalSpace γ₂<VAR>MeasurableSpace γ₂<VAR>BorelSpace γ₂<VAR>h : γ ≃ₜ γ₂<GOAL>MeasurableEmbedding ⇑h
<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>TopologicalSpace γ₂<VAR>MeasurableSpace γ₂<VAR>BorelSpace γ₂<VAR>h : γ ≃ₜ γ₂<GOAL>⇑h.toMeasurableEquiv = ⇑h
<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>TopologicalSpace γ₂<VAR>MeasurableSpace γ₂<VAR>BorelSpace γ₂<VAR>h : γ ≃ₜ γ₂<GOAL>⇑h.toMeasurableEquiv.symm = ⇑h.symm
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>f : C(α, γ)<GOAL>Measurable ⇑f
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>T1Space α<VAR>f : α → γ<VAR>a : α<VAR>hf : ContinuousOn f {a}ᶜ<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_5<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace β<VAR>MeasurableSpace β<VAR>OpensMeasurableSpace β<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>MeasurableSpace δ<VAR>SecondCountableTopologyEither α β<VAR>f : δ → α<VAR>g : δ → β<VAR>c : α → β → γ<VAR>h : Continuous fun p => c p.1 p.2<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun a => c (f a) (g a)