ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>ι : Type u_4<VAR>inst✝¹ : SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace ↥(U i)<VAR>hU : Monotone U<VAR>x : E<VAR>h✝ : Nonempty ι<VAR>y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)<VAR>proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>a : E<VAR>ha : a ∈ ⨆ i, U i<VAR>hay : ‖y - a‖ < ε<VAR>I : ι<VAR>hI : a ∈ U I<GOAL>∃ I, ∀ i ≥ I, ‖↑((orthogonalProjection (U i)) y) - y‖ < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>ι : Type u_4<VAR>inst✝¹ : SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace ↥(U i)<VAR>hU : Monotone U<VAR>x : E<VAR>h✝ : Nonempty ι<VAR>y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)<VAR>proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>a : E<VAR>ha : a ∈ ⨆ i, U i<VAR>hay : ‖y - a‖ < ε<VAR>I : ι<VAR>hI : a ∈ U I<VAR>i : ι<VAR>hi : I ≤ i<GOAL>‖↑((orthogonalProjection (U i)) y) - y‖ < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>ι : Type u_4<VAR>inst✝¹ : SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace ↥(U i)<VAR>hU : Monotone U<VAR>x : E<VAR>h✝ : Nonempty ι<VAR>y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)<VAR>proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>a : E<VAR>ha : a ∈ ⨆ i, U i<VAR>hay : ‖y - a‖ < ε<VAR>I : ι<VAR>hI : a ∈ U I<VAR>i : ι<VAR>hi : I ≤ i<GOAL>⨅ x, ‖y - ↑x‖ < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>ι : Type u_4<VAR>inst✝¹ : SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace ↥(U i)<VAR>hU : Monotone U<VAR>x : E<VAR>h✝ : Nonempty ι<VAR>y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)<VAR>proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>a : E<VAR>ha : a ∈ ⨆ i, U i<VAR>hay : ‖y - a‖ < ε<VAR>I : ι<VAR>hI : a ∈ U I<VAR>i : ι<VAR>hi : I ≤ i<GOAL>⨅ x, ‖y - ↑x‖ ≤ ‖y - a‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>ι : Type u_4<VAR>inst✝¹ : SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace ↥(U i)<VAR>hU : Monotone U<VAR>x : E<VAR>h✝ : Nonempty ι<VAR>y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)<VAR>proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>a : E<VAR>ha : a ∈ ⨆ i, U i<VAR>hay : ‖y - a‖ < ε<VAR>I : ι<VAR>hI : a ∈ U I<VAR>i : ι<VAR>hi : I ≤ i<GOAL>⨅ x, ‖y - ↑x‖ ≤ ‖y - ↑⟨a, ⋯⟩‖
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>z : ℤ<GOAL>IsUnit (A ^ z).det ↔ IsUnit A.det ∨ z = 0
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<GOAL>IsUnit (A ^ 0).det ↔ IsUnit A.det ∨ 0 = 0
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>z : ℕ<VAR>a✝ : IsUnit (A ^ ↑z).det ↔ IsUnit A.det ∨ ↑z = 0<GOAL>IsUnit (A ^ (↑z + 1)).det ↔ IsUnit A.det ∨ ↑z + 1 = 0
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>z : ℕ<VAR>a✝ : IsUnit (A ^ (-↑z)).det ↔ IsUnit A.det ∨ -↑z = 0<GOAL>IsUnit (A ^ (-↑z - 1)).det ↔ IsUnit A.det ∨ -↑z - 1 = 0
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x y : LocalizedModule S M<VAR>a a' : M<VAR>b b' : ↥S<GOAL>fromLocalizedModule' S f (LocalizedModule.mk a b + LocalizedModule.mk a' b') = fromLocalizedModule' S f (LocalizedModule.mk a b) + fromLocalizedModule' S f (LocalizedModule.mk a' b')
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x y : LocalizedModule S M<VAR>a a' : M<VAR>b b' : ↥S<GOAL>↑⋯.unit⁻¹ (f (b' • a + b • a')) = ↑⋯.unit⁻¹ (f a) + ↑⋯.unit⁻¹ (f a')
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x y : LocalizedModule S M<VAR>a a' : M<VAR>b b' : ↥S<GOAL>f (b' • a) + f (b • a') = ↑⋯.unit⁻¹ (f (↑(b * b') • a)) + ↑⋯.unit⁻¹ (↑(b * b') • f a')
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x y : LocalizedModule S M<VAR>a a' : M<VAR>b b' : ↥S<GOAL>f (b' • a) = ↑⋯.unit⁻¹ (f (↑(b * b') • a))
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x y : LocalizedModule S M<VAR>a a' : M<VAR>b b' : ↥S<GOAL>f (b • a') = ↑⋯.unit⁻¹ (↑(b * b') • f a')
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x y : LocalizedModule S M<VAR>a a' : M<VAR>b b' : ↥S<GOAL>f (↑(b * b') • a) = ↑b • f (b' • a)
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x y : LocalizedModule S M<VAR>a a' : M<VAR>b b' : ↥S<GOAL>↑(b * b') • f a' = ↑b' • f (b • a')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>l : Filter β<VAR>f : α → β<GOAL>Tendsto (fun x => f ↑x) atBot l ↔ Tendsto f (𝓝[>] a) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>l : Filter β<VAR>f : α → β<GOAL>Tendsto (fun x => f ↑x) atBot l ↔ Tendsto (f ∘ Subtype.val) atBot l
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α → ℝ≥0∞<VAR>g : β → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g ν<GOAL>∫⁻ (z : α × β), f z.1 * g z.2 ∂μ.prod ν = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν
<VAR>X✝ : Type u_1<VAR>Y✝ : Type u_2<VAR>inst✝⁵ : TopologicalSpace X✝<VAR>inst✝⁴ : FirstCountableTopology X✝<VAR>inst✝³ : R1Space X✝<VAR>x✝ y : X✝<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : R1Space Y<VAR>f : X → Y<VAR>x : X<VAR>K : Set X<VAR>s : Set Y<VAR>hf : Continuous f<VAR>hs : s ∈ 𝓝 (f x)<VAR>hKc : IsCompact K<VAR>hKx : K ∈ 𝓝 x<GOAL>∃ K ∈ 𝓝 x, IsCompact K ∧ MapsTo f K s
<VAR>X✝ : Type u_1<VAR>Y✝ : Type u_2<VAR>inst✝⁵ : TopologicalSpace X✝<VAR>inst✝⁴ : FirstCountableTopology X✝<VAR>inst✝³ : R1Space X✝<VAR>x✝ y : X✝<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : R1Space Y<VAR>f : X → Y<VAR>x : X<VAR>K : Set X<VAR>s : Set Y<VAR>hf : Continuous f<VAR>hs : s ∈ 𝓝 (f x)<VAR>hKc : IsCompact K<VAR>hKx : K ∈ 𝓝 x<VAR>hc : IsCompact (f '' K \ interior s)<GOAL>∃ K ∈ 𝓝 x, IsCompact K ∧ MapsTo f K s
<VAR>X✝ : Type u_1<VAR>Y✝ : Type u_2<VAR>inst✝⁵ : TopologicalSpace X✝<VAR>inst✝⁴ : FirstCountableTopology X✝<VAR>inst✝³ : R1Space X✝<VAR>x✝ y : X✝<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : R1Space Y<VAR>f : X → Y<VAR>x : X<VAR>K : Set X<VAR>s : Set Y<VAR>hf : Continuous f<VAR>hs : s ∈ 𝓝 (f x)<VAR>hKc : IsCompact K<VAR>hKx : K ∈ 𝓝 x<VAR>hc : IsCompact (f '' K \ interior s)<VAR>U V : Set Y<VAR>Uo : IsOpen U<VAR>Vo : IsOpen V<VAR>hxU : {f x} ⊆ U<VAR>hV : f '' K \ interior s ⊆ V<VAR>hd : Disjoint U V<GOAL>∃ K ∈ 𝓝 x, IsCompact K ∧ MapsTo f K s
<VAR>X✝ : Type u_1<VAR>Y✝ : Type u_2<VAR>inst✝⁵ : TopologicalSpace X✝<VAR>inst✝⁴ : FirstCountableTopology X✝<VAR>inst✝³ : R1Space X✝<VAR>x✝ y : X✝<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : R1Space Y<VAR>f : X → Y<VAR>x : X<VAR>K : Set X<VAR>s : Set Y<VAR>hf : Continuous f<VAR>hs : s ∈ 𝓝 (f x)<VAR>hKc : IsCompact K<VAR>hKx : K ∈ 𝓝 x<VAR>hc : IsCompact (f '' K \ interior s)<VAR>U V : Set Y<VAR>Uo : IsOpen U<VAR>Vo : IsOpen V<VAR>hxU : {f x} ⊆ U<VAR>hV : f '' K \ interior s ⊆ V<VAR>hd : Disjoint U V<GOAL>(f ⁻¹' V)ᶜ ∈ 𝓝 x
<VAR>X✝ : Type u_1<VAR>Y✝ : Type u_2<VAR>inst✝⁵ : TopologicalSpace X✝<VAR>inst✝⁴ : FirstCountableTopology X✝<VAR>inst✝³ : R1Space X✝<VAR>x✝ y✝ : X✝<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : R1Space Y<VAR>f : X → Y<VAR>x : X<VAR>K : Set X<VAR>s : Set Y<VAR>hf : Continuous f<VAR>hs : s ∈ 𝓝 (f x)<VAR>hKc : IsCompact K<VAR>hKx : K ∈ 𝓝 x<VAR>hc : IsCompact (f '' K \ interior s)<VAR>U V : Set Y<VAR>Uo : IsOpen U<VAR>Vo : IsOpen V<VAR>hxU : {f x} ⊆ U<VAR>hV : f '' K \ interior s ⊆ V<VAR>hd : Disjoint U V<VAR>y : X<VAR>hy : y ∈ K \ f ⁻¹' V<GOAL>f y ∈ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹⁶ : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹⁵ : TopologicalSpace X<VAR>inst✝¹⁴ : TopologicalSpace Y<VAR>inst✝¹³ : MeasurableSpace Y<VAR>inst✝¹² : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : FirstCountableTopology X<VAR>inst✝³ : LocallyCompactSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>inst✝¹ : SecondCountableTopologyEither Y E<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → Y → E<VAR>hf : Continuous (uncurry f)<VAR>s : Set Y<VAR>hs : IsCompact s<GOAL>Continuous fun x => ∫ (y : Y) in s, f x y ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹⁶ : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹⁵ : TopologicalSpace X<VAR>inst✝¹⁴ : TopologicalSpace Y<VAR>inst✝¹³ : MeasurableSpace Y<VAR>inst✝¹² : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : FirstCountableTopology X<VAR>inst✝³ : LocallyCompactSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>inst✝¹ : SecondCountableTopologyEither Y E<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → Y → E<VAR>hf : Continuous (uncurry f)<VAR>s : Set Y<VAR>hs : IsCompact s<GOAL>∀ (x : X), ContinuousAt (fun x => ∫ (y : Y) in s, f x y ∂μ) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹⁶ : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹⁵ : TopologicalSpace X<VAR>inst✝¹⁴ : TopologicalSpace Y<VAR>inst✝¹³ : MeasurableSpace Y<VAR>inst✝¹² : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : FirstCountableTopology X<VAR>inst✝³ : LocallyCompactSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>inst✝¹ : SecondCountableTopologyEither Y E<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → Y → E<VAR>hf : Continuous (uncurry f)<VAR>s : Set Y<VAR>hs : IsCompact s<VAR>x₀ : X<GOAL>ContinuousAt (fun x => ∫ (y : Y) in s, f x y ∂μ) x₀
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹⁶ : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹⁵ : TopologicalSpace X<VAR>inst✝¹⁴ : TopologicalSpace Y<VAR>inst✝¹³ : MeasurableSpace Y<VAR>inst✝¹² : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : FirstCountableTopology X<VAR>inst✝³ : LocallyCompactSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>inst✝¹ : SecondCountableTopologyEither Y E<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → Y → E<VAR>hf : Continuous (uncurry f)<VAR>s : Set Y<VAR>hs : IsCompact s<VAR>x₀ : X<VAR>U : Set X<VAR>U_cpct : IsCompact U<VAR>U_nhds : U ∈ 𝓝 x₀<GOAL>ContinuousAt (fun x => ∫ (y : Y) in s, f x y ∂μ) x₀
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹⁶ : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹⁵ : TopologicalSpace X<VAR>inst✝¹⁴ : TopologicalSpace Y<VAR>inst✝¹³ : MeasurableSpace Y<VAR>inst✝¹² : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : FirstCountableTopology X<VAR>inst✝³ : LocallyCompactSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>inst✝¹ : SecondCountableTopologyEither Y E<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → Y → E<VAR>hf : Continuous (uncurry f)<VAR>s : Set Y<VAR>hs : IsCompact s<VAR>x₀ : X<VAR>U : Set X<VAR>U_cpct : IsCompact U<VAR>U_nhds : U ∈ 𝓝 x₀<VAR>M : ℝ<VAR>hM : M ∈ upperBounds ((fun x => ‖uncurry f x‖) '' U ×ˢ s)<GOAL>ContinuousAt (fun x => ∫ (y : Y) in s, f x y ∂μ) x₀
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹⁶ : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹⁵ : TopologicalSpace X<VAR>inst✝¹⁴ : TopologicalSpace Y<VAR>inst✝¹³ : MeasurableSpace Y<VAR>inst✝¹² : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : FirstCountableTopology X<VAR>inst✝³ : LocallyCompactSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>inst✝¹ : SecondCountableTopologyEither Y E<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → Y → E<VAR>hf : Continuous (uncurry f)<VAR>s : Set Y<VAR>hs : IsCompact s<VAR>x₀ : X<VAR>U : Set X<VAR>U_cpct : IsCompact U<VAR>U_nhds : U ∈ 𝓝 x₀<VAR>M : ℝ<VAR>hM : M ∈ upperBounds ((fun x => ‖uncurry f x‖) '' U ×ˢ s)<GOAL>∀ᶠ (x : X) in 𝓝 x₀, AEStronglyMeasurable (f x) (μ.restrict s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹⁶ : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹⁵ : TopologicalSpace X<VAR>inst✝¹⁴ : TopologicalSpace Y<VAR>inst✝¹³ : MeasurableSpace Y<VAR>inst✝¹² : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : FirstCountableTopology X<VAR>inst✝³ : LocallyCompactSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>inst✝¹ : SecondCountableTopologyEither Y E<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → Y → E<VAR>hf : Continuous (uncurry f)<VAR>s : Set Y<VAR>hs : IsCompact s<VAR>x₀ : X<VAR>U : Set X<VAR>U_cpct : IsCompact U<VAR>U_nhds : U ∈ 𝓝 x₀<VAR>M : ℝ<VAR>hM : M ∈ upperBounds ((fun x => ‖uncurry f x‖) '' U ×ˢ s)<GOAL>∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : Y) ∂μ.restrict s, ‖f x a‖ ≤ ?intro.intro.intro.bound a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹⁶ : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹⁵ : TopologicalSpace X<VAR>inst✝¹⁴ : TopologicalSpace Y<VAR>inst✝¹³ : MeasurableSpace Y<VAR>inst✝¹² : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : FirstCountableTopology X<VAR>inst✝³ : LocallyCompactSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>inst✝¹ : SecondCountableTopologyEither Y E<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → Y → E<VAR>hf : Continuous (uncurry f)<VAR>s : Set Y<VAR>hs : IsCompact s<VAR>x₀ : X<VAR>U : Set X<VAR>U_cpct : IsCompact U<VAR>U_nhds : U ∈ 𝓝 x₀<VAR>M : ℝ<VAR>hM : M ∈ upperBounds ((fun x => ‖uncurry f x‖) '' U ×ˢ s)<GOAL>Integrable ?intro.intro.intro.bound (μ.restrict s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹⁶ : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹⁵ : TopologicalSpace X<VAR>inst✝¹⁴ : TopologicalSpace Y<VAR>inst✝¹³ : MeasurableSpace Y<VAR>inst✝¹² : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : FirstCountableTopology X<VAR>inst✝³ : LocallyCompactSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>inst✝¹ : SecondCountableTopologyEither Y E<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → Y → E<VAR>hf : Continuous (uncurry f)<VAR>s : Set Y<VAR>hs : IsCompact s<VAR>x₀ : X<VAR>U : Set X<VAR>U_cpct : IsCompact U<VAR>U_nhds : U ∈ 𝓝 x₀<VAR>M : ℝ<VAR>hM : M ∈ upperBounds ((fun x => ‖uncurry f x‖) '' U ×ˢ s)<GOAL>∀ᵐ (a : Y) ∂μ.restrict s, ContinuousAt (fun x => f x a) x₀
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹⁶ : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹⁵ : TopologicalSpace X<VAR>inst✝¹⁴ : TopologicalSpace Y<VAR>inst✝¹³ : MeasurableSpace Y<VAR>inst✝¹² : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : FirstCountableTopology X<VAR>inst✝³ : LocallyCompactSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>inst✝¹ : SecondCountableTopologyEither Y E<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → Y → E<VAR>hf : Continuous (uncurry f)<VAR>s : Set Y<VAR>hs : IsCompact s<VAR>x₀ : X<VAR>U : Set X<VAR>U_cpct : IsCompact U<VAR>U_nhds : U ∈ 𝓝 x₀<VAR>M : ℝ<VAR>hM : M ∈ upperBounds ((fun x => ‖uncurry f x‖) '' U ×ˢ s)<GOAL>Y → ℝ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>N : LieSubmodule R L M<GOAL>baseChange A ⊤ = ⊤
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>N : LieSubmodule R L M<GOAL>{ toSubmodule := ⊤, lie_mem := ⋯ } = ⊤
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R I J X Y R₁ R₂ : Set α<VAR>M : Matroid α<VAR>hR : R₂ ⊆ R₁<GOAL>M ↾ R₁ ↾ R₂ = M ↾ R₂
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R I J X Y R₁ R₂ : Set α<VAR>M : Matroid α<VAR>hR : R₂ ⊆ R₁<GOAL>∀ I ⊆ (M ↾ R₁ ↾ R₂).E, (M ↾ R₁ ↾ R₂).Indep I ↔ (M ↾ R₂).Indep I
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R I J X Y R₁ R₂ : Set α<VAR>M : Matroid α<VAR>hR : R₂ ⊆ R₁<GOAL>∀ I ⊆ R₂, I ⊆ R₂ → M.Indep I → I ⊆ R₁
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hw : ∑ i ∈ t, w i = 1<GOAL>t.centerMass w z = ∑ i ∈ t, w i • z i