ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>x : E<VAR>r : ℝ<GOAL>μ (Metric.ball x r) = μ (Metric.ball 0 r)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>x : E<VAR>r : ℝ<GOAL>μ (Metric.closedBall x r) = μ (Metric.closedBall 0 r)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>s : ℝ<GOAL>μ (Metric.ball x (r * s)) = ENNReal.ofReal (r ^ FiniteDimensional.finrank ℝ E) * μ (Metric.ball 0 s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>μ (Metric.ball x r) = ENNReal.ofReal (r ^ FiniteDimensional.finrank ℝ E) * μ (Metric.ball 0 1)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>s : ℝ<GOAL>μ (Metric.ball x (r * s)) = ENNReal.ofReal (r ^ FiniteDimensional.finrank ℝ E) * μ (Metric.ball 0 s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>μ (Metric.ball x r) = ENNReal.ofReal (r ^ FiniteDimensional.finrank ℝ E) * μ (Metric.ball 0 1)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>s : ℝ<GOAL>μ (Metric.closedBall x (r * s)) = ENNReal.ofReal (r ^ FiniteDimensional.finrank ℝ E) * μ (Metric.closedBall 0 s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>s : ℝ<VAR>hs : 0 ≤ s<GOAL>μ (Metric.closedBall x (r * s)) = ENNReal.ofReal (r ^ FiniteDimensional.finrank ℝ E) * μ (Metric.closedBall 0 s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>μ (Metric.closedBall x r) = ENNReal.ofReal (r ^ FiniteDimensional.finrank ℝ E) * μ (Metric.closedBall 0 1)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<GOAL>μ (Metric.closedBall 0 1) = μ (Metric.ball 0 1)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>μ (Metric.closedBall x r) = ENNReal.ofReal (r ^ FiniteDimensional.finrank ℝ E) * μ (Metric.ball 0 1)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>μ (Metric.closedBall x r) = μ (Metric.ball x r)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>μ (Metric.sphere x r) = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>μ (Metric.sphere x r) = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>x y : E<VAR>s t : Set E<GOAL>μ ({x} + r • s) / μ ({y} + r • t) = μ s / μ t
<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>b : Basis ι ℝ G<VAR>v : ι → G<GOAL>b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v|
<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>FiniteDimensional ℝ G<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank ℝ G = n)<VAR>ω : G [⋀^Fin n]→ₗ[ℝ] ℝ<GOAL>ω.measure = ‖ω ⇑(FiniteDimensional.finBasisOfFinrankEq ℝ G ⋯)‖₊ • (FiniteDimensional.finBasisOfFinrankEq ℝ G ⋯).addHaar
<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>FiniteDimensional ℝ G<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank ℝ G = n)<VAR>ω : G [⋀^Fin n]→ₗ[ℝ] ℝ<VAR>v : Fin n → G<GOAL>ω.measure (parallelepiped v) = ENNReal.ofReal |ω v|
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>s : Set E<VAR>x : E<VAR>h : Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>t_bound : t ⊆ Metric.closedBall 0 1<GOAL>Filter.Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>s : Set E<VAR>x : E<VAR>h : Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>t_bound : t ⊆ Metric.closedBall 0 R<GOAL>Filter.Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>s : Set E<VAR>x : E<VAR>h : Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h''t : μ t ≠ ⊤<GOAL>Filter.Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>s : Set E<VAR>hs : MeasurableSet s<VAR>x : E<VAR>h : Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>h''t : μ t ≠ ⊤<GOAL>Filter.Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>s : Set E<VAR>x : E<VAR>h : Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>h''t : μ t ≠ ⊤<GOAL>Filter.Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>s : Set E<VAR>x : E<VAR>h : Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<GOAL>∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • t)).Nonempty
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>x y : WithLp 2 (E × F)<GOAL>⟪x, y⟫_𝕜 = ⟪x.1, y.1⟫_𝕜 + ⟪x.2, y.2⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>Fintype ι₁<VAR>Fintype ι₂<VAR>v : OrthonormalBasis ι₁ 𝕜 E<VAR>w : OrthonormalBasis ι₂ 𝕜 F<VAR>i : ι₁ ⊕ ι₂<GOAL>(v.prod w) i = Sum.elim (⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) i
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ E<VAR>InnerProductSpace ℝ F<VAR>f : E →L[ℝ] F<GOAL>IsConformalMap f ↔ ∃ c, 0 < c ∧ ∀ (u v : E), ⟪f u, f v⟫_ℝ = c * ⟪u, v⟫_ℝ
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>T2Space E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<VAR>r : ℝ<GOAL>Euclidean.ball x r = ⇑toEuclidean ⁻¹' Metric.ball (toEuclidean x) r
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>T2Space E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<VAR>r : ℝ<GOAL>Euclidean.closedBall x r = ⇑toEuclidean ⁻¹' Metric.closedBall (toEuclidean x) r
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>T2Space E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<VAR>r : ℝ<GOAL>Euclidean.ball x r ⊆ Euclidean.closedBall x r
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>T2Space E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<VAR>r : ℝ<GOAL>IsOpen (Euclidean.ball x r)
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>T2Space E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>x ∈ Euclidean.ball x r
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>T2Space E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<VAR>r : ℝ<GOAL>Euclidean.closedBall x r = ⇑toEuclidean.symm '' Metric.closedBall (toEuclidean x) r
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>T2Space E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<VAR>r : ℝ<GOAL>IsCompact (Euclidean.closedBall x r)
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>T2Space E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<VAR>r : ℝ<GOAL>IsClosed (Euclidean.closedBall x r)
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>T2Space E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<VAR>r : ℝ<VAR>h : r ≠ 0<GOAL>closure (Euclidean.ball x r) = Euclidean.closedBall x r
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>T2Space E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>FiniteDimensional ℝ E<VAR>R : ℝ<VAR>s : Set E<VAR>x : E<VAR>hR : 0 < R<VAR>hs : IsClosed s<VAR>h : s ⊆ Euclidean.ball x R<GOAL>∃ r ∈ Set.Ioo 0 R, s ⊆ Euclidean.ball x r
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>T2Space E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<GOAL>(𝓝 x).HasBasis (fun r => 0 < r) (Euclidean.closedBall x)
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>T2Space E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>Euclidean.closedBall x r ∈ 𝓝 x
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>T2Space E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<GOAL>(𝓝 x).HasBasis (fun r => 0 < r) (Euclidean.ball x)
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>T2Space E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>Euclidean.ball x r ∈ 𝓝 x
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>G : Type u_3<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>FiniteDimensional ℝ G<VAR>f g : F → G<VAR>n : ℕ∞<VAR>hf : ContDiff ℝ n f<VAR>hg : ContDiff ℝ n g<VAR>h : ∀ (x : F), f x ≠ g x<GOAL>ContDiff ℝ n fun x => Euclidean.dist (f x) (g x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : AnalyticAt 𝕜 f x<GOAL>MeromorphicAt f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>MeromorphicAt id x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>e : E<VAR>x : 𝕜<GOAL>MeromorphicAt (fun x => e) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>hg : MeromorphicAt g x<GOAL>MeromorphicAt (f + g) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → 𝕜<VAR>g : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>hg : MeromorphicAt g x<GOAL>MeromorphicAt (f • g) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>f g : 𝕜 → 𝕜<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>hg : MeromorphicAt g x<GOAL>MeromorphicAt (f * g) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<GOAL>MeromorphicAt (-f) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<GOAL>MeromorphicAt (-f) x ↔ MeromorphicAt f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>hg : MeromorphicAt g x<GOAL>MeromorphicAt (f - g) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>hfg : f =ᶠ[𝓝[≠] x] g<GOAL>MeromorphicAt g x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>f : 𝕜 → 𝕜<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<GOAL>MeromorphicAt f⁻¹ x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>f : 𝕜 → 𝕜<VAR>x : 𝕜<GOAL>MeromorphicAt f⁻¹ x ↔ MeromorphicAt f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>f g : 𝕜 → 𝕜<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>hg : MeromorphicAt g x<GOAL>MeromorphicAt (f / g) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>f : 𝕜 → 𝕜<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>n : ℕ<GOAL>MeromorphicAt (f ^ n) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>f : 𝕜 → 𝕜<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>n : ℤ<GOAL>MeromorphicAt (f ^ n) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<GOAL>hf.order = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>n : ℤ<GOAL>hf.order = ↑n ↔ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : AnalyticAt 𝕜 f x<GOAL>⋯.order = WithTop.map Nat.cast hf.order
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<GOAL>MeromorphicAt f x ↔ ∃ n g, AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>U : Set 𝕜<VAR>hf : AnalyticOn 𝕜 f U<GOAL>MeromorphicOn f U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>U : Set 𝕜<GOAL>MeromorphicOn id U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>e : E<VAR>U : Set 𝕜<GOAL>MeromorphicOn (fun x => e) U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>U : Set 𝕜<VAR>hf : MeromorphicOn f U<VAR>V : Set 𝕜<VAR>hv : V ⊆ U<GOAL>MeromorphicOn f V
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>U : Set 𝕜<VAR>hf : MeromorphicOn f U<VAR>hg : MeromorphicOn g U<GOAL>MeromorphicOn (f + g) U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>U : Set 𝕜<VAR>hf : MeromorphicOn f U<VAR>hg : MeromorphicOn g U<GOAL>MeromorphicOn (f - g) U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>U : Set 𝕜<VAR>hf : MeromorphicOn f U<GOAL>MeromorphicOn (-f) U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>U : Set 𝕜<GOAL>MeromorphicOn (-f) U ↔ MeromorphicOn f U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : 𝕜 → 𝕜<VAR>f : 𝕜 → E<VAR>U : Set 𝕜<VAR>hs : MeromorphicOn s U<VAR>hf : MeromorphicOn f U<GOAL>MeromorphicOn (s • f) U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>s t : 𝕜 → 𝕜<VAR>U : Set 𝕜<VAR>hs : MeromorphicOn s U<VAR>ht : MeromorphicOn t U<GOAL>MeromorphicOn (s * t) U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>s : 𝕜 → 𝕜<VAR>U : Set 𝕜<VAR>hs : MeromorphicOn s U<GOAL>MeromorphicOn s⁻¹ U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>s : 𝕜 → 𝕜<VAR>U : Set 𝕜<GOAL>MeromorphicOn s⁻¹ U ↔ MeromorphicOn s U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>s t : 𝕜 → 𝕜<VAR>U : Set 𝕜<VAR>hs : MeromorphicOn s U<VAR>ht : MeromorphicOn t U<GOAL>MeromorphicOn (s / t) U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>s : 𝕜 → 𝕜<VAR>U : Set 𝕜<VAR>hs : MeromorphicOn s U<VAR>n : ℕ<GOAL>MeromorphicOn (s ^ n) U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>s : 𝕜 → 𝕜<VAR>U : Set 𝕜<VAR>hs : MeromorphicOn s U<VAR>n : ℤ<GOAL>MeromorphicOn (s ^ n) U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>U : Set 𝕜<VAR>hf : MeromorphicOn f U<VAR>h_eq : Set.EqOn f g U<VAR>hu : IsOpen U<GOAL>MeromorphicOn g U
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>MeasureTheory.IsFiniteMeasure ν<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<GOAL>(p.prod q).radius = min p.radius q.radius
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>r s : ℝ≥0∞<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesOnBall f p e r<VAR>hg : HasFPowerSeriesOnBall g q e s<GOAL>HasFPowerSeriesOnBall (fun x => (f x, g x)) (p.prod q) e (min r s)
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesAt f p e<VAR>hg : HasFPowerSeriesAt g q e<GOAL>HasFPowerSeriesAt (fun x => (f x, g x)) (p.prod q) e
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>hf : AnalyticAt 𝕜 f e<VAR>hg : AnalyticAt 𝕜 g e<GOAL>AnalyticAt 𝕜 (fun x => (f x, g x)) e
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>g : E → G<VAR>s : Set E<VAR>hf : AnalyticOn 𝕜 f s<VAR>hg : AnalyticOn 𝕜 g s<GOAL>AnalyticOn 𝕜 (fun x => (f x, g x)) s
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>h : F × G → H<VAR>f : E → F<VAR>g : E → G<VAR>x : E<VAR>ha : AnalyticAt 𝕜 h (f x, g x)<VAR>fa : AnalyticAt 𝕜 f x<VAR>ga : AnalyticAt 𝕜 g x<GOAL>AnalyticAt 𝕜 (fun x => h (f x, g x)) x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>h : F × G → H<VAR>f : E → F<VAR>g : E → G<VAR>s : Set (F × G)<VAR>t : Set E<VAR>ha : AnalyticOn 𝕜 h s<VAR>fa : AnalyticOn 𝕜 f t<VAR>ga : AnalyticOn 𝕜 g t<VAR>m : ∀ x ∈ t, (f x, g x) ∈ s<GOAL>AnalyticOn 𝕜 (fun x => h (f x, g x)) t
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>p : E × F<VAR>fa : AnalyticAt 𝕜 f p<GOAL>AnalyticAt 𝕜 (fun x => f (x, p.2)) p.1
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>p : E × F<VAR>fa : AnalyticAt 𝕜 f p<GOAL>AnalyticAt 𝕜 (fun y => f (p.1, y)) p.2
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>s : Set (E × F)<VAR>y : F<VAR>fa : AnalyticOn 𝕜 f s<GOAL>AnalyticOn 𝕜 (fun x => f (x, y)) {x | (x, y) ∈ s}
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>x : E<VAR>s : Set (E × F)<VAR>fa : AnalyticOn 𝕜 f s<GOAL>AnalyticOn 𝕜 (fun y => f (x, y)) {y | (x, y) ∈ s}
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕝 : Type u_7<VAR>NontriviallyNormedField 𝕝<VAR>NormedAlgebra 𝕜 𝕝<VAR>NormedSpace 𝕝 E<VAR>IsScalarTower 𝕜 𝕝 E<VAR>z : 𝕝 × E<GOAL>AnalyticAt 𝕜 (fun x => x.1 • x.2) z
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>A : Type u_8<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>z : A × A<GOAL>AnalyticAt 𝕜 (fun x => x.1 * x.2) z