ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type (max (max (max uE u𝕜) uι) (max uE uι) u𝕜) := (⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)<VAR>G' : Submodule 𝕜 F := LinearMap.range (lift f.toMultilinearMap)<VAR>e : ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) ≃ₗ[𝕜] ↥(LinearMap.range (lift f.toMultilinearMap)) := (lift f.toMultilinearMap).quotKerEquivRange<VAR>this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e<VAR>this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e<VAR>f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)<VAR>hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖<VAR>f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := f'₀.mkContinuous ‖f‖ hf'₀<VAR>hnorm : ‖f'‖ ≤ ‖f‖<VAR>heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x<VAR>hle : (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) ≤ injectiveSeminorm<GOAL>‖(lift f'.toMultilinearMap) x‖ ≤ ‖f'‖ * (fun f => ⇑f) ((normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)) x
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type (max (max (max uE u𝕜) uι) (max uE uι) u𝕜) := (⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)<VAR>G' : Submodule 𝕜 F := LinearMap.range (lift f.toMultilinearMap)<VAR>e : ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) ≃ₗ[𝕜] ↥(LinearMap.range (lift f.toMultilinearMap)) := (lift f.toMultilinearMap).quotKerEquivRange<VAR>this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e<VAR>this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e<VAR>f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)<VAR>hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖<VAR>f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := f'₀.mkContinuous ‖f‖ hf'₀<VAR>hnorm : ‖f'‖ ≤ ‖f‖<VAR>heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x<VAR>hle : (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) ≤ injectiveSeminorm<GOAL>‖((toDualContinuousMultilinearMap ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap))) x) f'‖ ≤ ‖f'‖ * ‖(toDualContinuousMultilinearMap G) x‖
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type (max (max (max uE u𝕜) uι) (max uE uι) u𝕜) := (⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)<VAR>G' : Submodule 𝕜 F := LinearMap.range (lift f.toMultilinearMap)<VAR>e : ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) ≃ₗ[𝕜] ↥(LinearMap.range (lift f.toMultilinearMap)) := (lift f.toMultilinearMap).quotKerEquivRange<VAR>this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e<VAR>this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e<VAR>f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)<VAR>hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖<VAR>f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := f'₀.mkContinuous ‖f‖ hf'₀<VAR>hnorm : ‖f'‖ ≤ ‖f‖<VAR>heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x<VAR>hle : (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) ≤ injectiveSeminorm<GOAL>‖((toDualContinuousMultilinearMap ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap))) x) f'‖ ≤ ‖(toDualContinuousMultilinearMap G) x‖ * ‖f'‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>σ : ℝ<VAR>f : ℝ → E<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hf : MellinConvergent f ↑σ<VAR>hFf : VerticalIntegrable (mellin f) σ volume<VAR>hfx : ContinuousAt f x<VAR>g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))<GOAL>mellinInv σ (mellin f) x = f x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>σ : ℝ<VAR>f : ℝ → E<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hFf : VerticalIntegrable (mellin f) σ volume<VAR>hfx : ContinuousAt f x<VAR>g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))<VAR>hf : Integrable g volume<GOAL>mellinInv σ (mellin f) x = f x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>σ : ℝ<VAR>f : ℝ → E<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hfx : ContinuousAt f x<VAR>g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))<VAR>hf : Integrable g volume<VAR>hFf : Integrable (𝓕 g) volume<GOAL>mellinInv σ (mellin f) x = f x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>σ : ℝ<VAR>f : ℝ → E<VAR>x : ℝ<VAR>hx : 0 < x<VAR>g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))<VAR>hf : Integrable g volume<VAR>hFf : Integrable (𝓕 g) volume<VAR>hfx : ContinuousAt g (-Real.log x)<GOAL>mellinInv σ (mellin f) x = f x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : ContDiffWithinAt 𝕜 n f s x<GOAL>ContinuousWithinAt f s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p✝ : E → FormalMultilinearSeries 𝕜 E F<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>H : HasFTaylorSeriesUpToOn (↑0) f p u<GOAL>ContinuousWithinAt f s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p✝ : E → FormalMultilinearSeries 𝕜 E F<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>u : Set E<VAR>hu : x ∈ u ∧ u ∈ 𝓝[s] x<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>H : HasFTaylorSeriesUpToOn (↑0) f p u<GOAL>ContinuousWithinAt f s x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : ClosedIciTopology α<VAR>inst✝ : TopologicalSpace β<VAR>a b c : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Ioc a b) a ↔ ContinuousWithinAt f (Ioi a) a
<VAR>z τ : ℂ<VAR>hτ : τ.im ≤ 0<GOAL>jacobiTheta₂_fderiv z τ = 0
<VAR>z τ : ℂ<VAR>hτ : τ.im ≤ 0<GOAL>¬Summable fun b => jacobiTheta₂_term_fderiv b z τ
<VAR>z τ : ℂ<VAR>hτ : τ.im ≤ 0<GOAL>¬0 < τ.im
<VAR>α : Type u_1<VAR>a b : ℕ<VAR>h₁ : delta * a < b<VAR>h₂ : delta * b < a<GOAL>a ≤ delta * (delta * a)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A B C : Matrix n n R<VAR>hC : C.det = 1<VAR>hA : A = B * C<GOAL>B.det * C.det = B.det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝² : AddMonoid α<VAR>inst✝¹ : Group γ<VAR>inst✝ : DistribMulAction γ α<VAR>h : Periodic f c<VAR>a : γ<GOAL>Periodic (fun x => f (a⁻¹ • x)) (a • c)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s t : Set α<VAR>h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤<GOAL>(OuterMeasure.ofFunction m m_empty) (s ∪ t) = (OuterMeasure.ofFunction m m_empty) s + (OuterMeasure.ofFunction m m_empty) t
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s t : Set α<VAR>h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤<VAR>f : ℕ → Set α<VAR>hf : s ∪ t ⊆ ⋃ i, f i<GOAL>(OuterMeasure.ofFunction m m_empty) s + (OuterMeasure.ofFunction m m_empty) t ≤ ∑' (i : ℕ), m (f i)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s t : Set α<VAR>h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤<VAR>f : ℕ → Set α<VAR>hf : s ∪ t ⊆ ⋃ i, f i<VAR>μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty<GOAL>μ s + μ t ≤ ∑' (i : ℕ), m (f i)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s t : Set α<VAR>h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤<VAR>f : ℕ → Set α<VAR>hf : s ∪ t ⊆ ⋃ i, f i<VAR>μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty<VAR>i : ℕ<VAR>hs : (s ∩ f i).Nonempty<VAR>ht : (t ∩ f i).Nonempty<GOAL>μ s + μ t ≤ ∑' (i : ℕ), m (f i)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s t : Set α<VAR>h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤<VAR>f : ℕ → Set α<VAR>hf : s ∪ t ⊆ ⋃ i, f i<VAR>μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty<VAR>he : ¬∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty<GOAL>μ s + μ t ≤ ∑' (i : ℕ), m (f i)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s t : Set α<VAR>h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤<VAR>f : ℕ → Set α<VAR>hf : s ∪ t ⊆ ⋃ i, f i<VAR>μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty<VAR>he : ¬∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty<VAR>I : Set α → Set ℕ := fun s => {i | (s ∩ f i).Nonempty}<GOAL>μ s + μ t ≤ ∑' (i : ℕ), m (f i)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s t : Set α<VAR>h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤<VAR>f : ℕ → Set α<VAR>hf : s ∪ t ⊆ ⋃ i, f i<VAR>μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty<VAR>he : ¬∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty<VAR>I : Set α → Set ℕ := fun s => {i | (s ∩ f i).Nonempty}<VAR>hd : Disjoint (I s) (I t)<GOAL>μ s + μ t ≤ ∑' (i : ℕ), m (f i)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s t : Set α<VAR>h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤<VAR>f : ℕ → Set α<VAR>hf : s ∪ t ⊆ ⋃ i, f i<VAR>μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty<VAR>he : ¬∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty<VAR>I : Set α → Set ℕ := fun s => {i | (s ∩ f i).Nonempty}<VAR>hd : Disjoint (I s) (I t)<VAR>hI : ∀ u ⊆ s ∪ t, μ u ≤ ∑' (i : ↑(I u)), μ (f ↑i)<GOAL>μ s + μ t ≤ ∑' (i : ℕ), m (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : IsSFiniteKernel κ<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>(μ ⊗ₘ κ) s = ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' s) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : IsSFiniteKernel κ<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : α), (κ b) {c | (b, c) ∈ s} ∂μ = ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' s) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m✝ : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), NullMeasurableSet (s i) μ<VAR>H : μ univ < ∑' (i : ι), μ (s i)<GOAL>∃ i j, i ≠ j ∧ (s i ∩ s j).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m✝ : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), NullMeasurableSet (s i) μ<VAR>H : ∀ (i j : ι), i ≠ j → s i ∩ s j = ∅<GOAL>∑' (i : ι), μ (s i) ≤ μ univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m✝ : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), NullMeasurableSet (s i) μ<VAR>H : ∀ (i j : ι), i ≠ j → s i ∩ s j = ∅<GOAL>Pairwise (AEDisjoint μ on s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m✝ : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), NullMeasurableSet (s i) μ<VAR>H : ∀ (i j : ι), i ≠ j → s i ∩ s j = ∅<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>(AEDisjoint μ on s) i j
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>f : α → β<GOAL>map (fun i => f ↑i) l.attach = map f l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>f : α → β<GOAL>pmap (fun a h => f ↑⟨a, h⟩) l ⋯ = map f l
<VAR>n : ℕ<VAR>α α' β β' : TypeVec.{u_1} n<VAR>f : α ⟹ β<VAR>g : α' ⟹ β'<GOAL>prod.snd ⊚ (f ⊗' g) = g ⊚ prod.snd
<VAR>n : ℕ<VAR>α α' β β' : TypeVec.{u_1} n<VAR>f : α ⟹ β<VAR>g : α' ⟹ β'<VAR>i : Fin2 n<GOAL>(prod.snd ⊚ (f ⊗' g)) i = (g ⊚ prod.snd) i
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : 0 < n<GOAL>log p n = padicValNat p n ↔ n < p ^ (padicValNat p n + 1)
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : 0 < n<GOAL>n < p ^ (padicValNat p n + 1) → p ^ padicValNat p n ≤ n
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a b : ι → ℝ<VAR>h : a ≤ b<GOAL>(volume (univ.pi fun i => Ioo (a i) (b i))).toReal = ∏ i : ι, (b i - a i)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>mulETransformRight e⁻¹ x = (mulETransformLeft e x.swap).swap
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : StarRing R<VAR>inst✝¹⁵ : NonUnitalSemiring A<VAR>inst✝¹⁴ : StarRing A<VAR>inst✝¹³ : Module R A<VAR>inst✝¹² : IsScalarTower R A A<VAR>inst✝¹¹ : SMulCommClass R A A<VAR>inst✝¹⁰ : StarModule R A<VAR>inst✝⁹ : NonUnitalSemiring B<VAR>inst✝⁸ : StarRing B<VAR>inst✝⁷ : Module R B<VAR>inst✝⁶ : IsScalarTower R B B<VAR>inst✝⁵ : SMulCommClass R B B<VAR>inst✝⁴ : StarModule R B<VAR>inst✝³ : FunLike F A B<VAR>inst✝² : NonUnitalAlgHomClass F R A B<VAR>inst✝¹ : NonUnitalStarAlgHomClass F R A B<VAR>S : NonUnitalStarSubalgebra R A<VAR>ι : Type u_1<VAR>inst✝ : Nonempty ι<VAR>K : ι → NonUnitalStarSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)<VAR>i : ι<VAR>x : ↥(K i)<VAR>h : K i ≤ iSup K<GOAL>Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑(iSup K) ⋯ ((inclusion h) x) = (f i) x
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : StarRing R<VAR>inst✝¹⁵ : NonUnitalSemiring A<VAR>inst✝¹⁴ : StarRing A<VAR>inst✝¹³ : Module R A<VAR>inst✝¹² : IsScalarTower R A A<VAR>inst✝¹¹ : SMulCommClass R A A<VAR>inst✝¹⁰ : StarModule R A<VAR>inst✝⁹ : NonUnitalSemiring B<VAR>inst✝⁸ : StarRing B<VAR>inst✝⁷ : Module R B<VAR>inst✝⁶ : IsScalarTower R B B<VAR>inst✝⁵ : SMulCommClass R B B<VAR>inst✝⁴ : StarModule R B<VAR>inst✝³ : FunLike F A B<VAR>inst✝² : NonUnitalAlgHomClass F R A B<VAR>inst✝¹ : NonUnitalStarAlgHomClass F R A B<VAR>S : NonUnitalStarSubalgebra R A<VAR>ι : Type u_1<VAR>inst✝ : Nonempty ι<VAR>K : ι → NonUnitalStarSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)<VAR>i : ι<VAR>x : ↥(K i)<VAR>h : K i ≤ iSup K<GOAL>↑(K i) ⊆ ↑(iSup K)
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>χ : MulChar R R'<VAR>a✝ : Rˣ<GOAL>(1 * χ) ↑a✝ = χ ↑a✝
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ : List α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>finj : Injective f<VAR>l₁ l₂ : List α<GOAL>map f (l₁.diff l₂) = (map f l₁).diff (map f l₂)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidableEq α<VAR>h : a ≤ b<GOAL>Icc a b \ Ico a b = {b}
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : Fintype Rˣ<VAR>a : Rˣ<VAR>χ : MulChar R R'<GOAL>(equivToUnitHom χ) a ∈ rootsOfUnity ⟨Fintype.card Rˣ, ⋯⟩ R'
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ : Seminorm 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>(s.sup p).closedBall x r = s.inf fun i => (p i).closedBall x r
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ : Seminorm 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>(s.sup p).closedBall x r = ⨅ a ∈ s, (p a).closedBall x r
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>x : α<VAR>adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t<VAR>s : Set α<VAR>hs : s ∈ 𝓝 x<GOAL>s ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>x : α<VAR>adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t<VAR>s : Set α<VAR>hs : s ∈ 𝓝 x<VAR>U : Set (α × α)<VAR>U_mem : U ∈ 𝓤 α<VAR>hU : U ○ U ⊆ {p | p.1 = x → p.2 ∈ s}<GOAL>s ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>x : α<VAR>adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t<VAR>s : Set α<VAR>hs : s ∈ 𝓝 x<VAR>U : Set (α × α)<VAR>U_mem : U ∈ 𝓤 α<VAR>hU : U ○ U ⊆ {p | p.1 = x → p.2 ∈ s}<VAR>t : Set α<VAR>t_mem : t ∈ f<VAR>ht : t ×ˢ t ⊆ U<VAR>y : α<VAR>hxy : (x, y) ∈ U<VAR>hy : y ∈ t<GOAL>s ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>x : α<VAR>adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t<VAR>s : Set α<VAR>hs : s ∈ 𝓝 x<VAR>U : Set (α × α)<VAR>U_mem : U ∈ 𝓤 α<VAR>hU : U ○ U ⊆ {p | p.1 = x → p.2 ∈ s}<VAR>t : Set α<VAR>t_mem : t ∈ f<VAR>ht : t ×ˢ t ⊆ U<VAR>y : α<VAR>hxy : (x, y) ∈ U<VAR>hy : y ∈ t<GOAL>t ⊆ s
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<GOAL>map g (I * J) = map g I * map g J
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<GOAL>map g ⟨↑I * ↑J, ⋯⟩ = ⟨↑(map g I) * ↑(map g J), ⋯⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>b ∈ Icc a b ↔ a ≤ b
<VAR>s : ℝ<GOAL>Gamma s * Gamma (1 - s) = π / sin (π * s)
<VAR>s : ℝ<GOAL>Complex.Gamma ↑s * Complex.Gamma (1 - ↑s) = ↑π / Complex.sin (↑π * ↑s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : OrderedAddCommMonoid M<VAR>inst✝¹ : OrderClosedTopology M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (b : β), MeasurableSet (f b)<VAR>hf₂ : ∀ (b : β), v.restrict (f b) ≤ w.restrict (f b)<GOAL>v.restrict (⋃ b, f b) ≤ w.restrict (⋃ b, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : OrderedAddCommMonoid M<VAR>inst✝¹ : OrderClosedTopology M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (b : β), MeasurableSet (f b)<VAR>hf₂ : ∀ (b : β), v.restrict (f b) ≤ w.restrict (f b)<VAR>val✝ : Encodable β<GOAL>v.restrict (⋃ b, f b) ≤ w.restrict (⋃ b, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : OrderedAddCommMonoid M<VAR>inst✝¹ : OrderClosedTopology M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (b : β), MeasurableSet (f b)<VAR>hf₂ : ∀ (b : β), v.restrict (f b) ≤ w.restrict (f b)<VAR>val✝ : Encodable β<GOAL>v.restrict (⋃ i, ⋃ b ∈ Encodable.decode₂ β i, f b) ≤ w.restrict (⋃ i, ⋃ b ∈ Encodable.decode₂ β i, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : OrderedAddCommMonoid M<VAR>inst✝¹ : OrderClosedTopology M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (b : β), MeasurableSet (f b)<VAR>hf₂ : ∀ (b : β), v.restrict (f b) ≤ w.restrict (f b)<VAR>val✝ : Encodable β<GOAL>∀ (n : ℕ), MeasurableSet (⋃ b ∈ Encodable.decode₂ β n, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : OrderedAddCommMonoid M<VAR>inst✝¹ : OrderClosedTopology M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (b : β), MeasurableSet (f b)<VAR>hf₂ : ∀ (b : β), v.restrict (f b) ≤ w.restrict (f b)<VAR>val✝ : Encodable β<GOAL>∀ (n : ℕ), v.restrict (⋃ b ∈ Encodable.decode₂ β n, f b) ≤ w.restrict (⋃ b ∈ Encodable.decode₂ β n, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>a : Ordinal.{max v u}<GOAL>a < lsub f ↔ ∃ i, a ≤ f i