ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : SecondCountableTopology X<VAR>B : Set (Set X)<VAR>hBc : B.Countable<VAR>hB : IsTopologicalBasis B<VAR>s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure UV.1 ⊆ UV.2}<VAR>this✝¹ : Encodable ↑s<VAR>this✝ : TopologicalSpace ↑s := ⊥<VAR>this : DiscreteTopology ↑s<VAR>hd : ∀ (UV : ↑s), Disjoint (closure (↑UV).1) (↑UV).2ᶜ<VAR>ε : ↑s → ℝ<VAR>ε01 : ∀ (UV : ↑s), ε UV ∈ Ioc 0 1<VAR>hε : Tendsto ε cofinite (𝓝 0)<VAR>f : ↑s → C(X, ℝ)<VAR>hf0 : ∀ (UV : ↑s), EqOn (⇑(f UV)) 0 (↑UV).1<VAR>hfε : ∀ (UV : ↑s), EqOn (⇑(f UV)) (fun x => ε UV) (↑UV).2ᶜ<VAR>hf0ε : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 (ε UV)<VAR>hf01 : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 1<GOAL>∃ f, Inducing f
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : SecondCountableTopology X<VAR>B : Set (Set X)<VAR>hBc : B.Countable<VAR>hB : IsTopologicalBasis B<VAR>s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure UV.1 ⊆ UV.2}<VAR>this✝¹ : Encodable ↑s<VAR>this✝ : TopologicalSpace ↑s := ⊥<VAR>this : DiscreteTopology ↑s<VAR>hd : ∀ (UV : ↑s), Disjoint (closure (↑UV).1) (↑UV).2ᶜ<VAR>ε : ↑s → ℝ<VAR>ε01 : ∀ (UV : ↑s), ε UV ∈ Ioc 0 1<VAR>hε : Tendsto ε cofinite (𝓝 0)<VAR>f : ↑s → C(X, ℝ)<VAR>hf0 : ∀ (UV : ↑s), EqOn (⇑(f UV)) 0 (↑UV).1<VAR>hfε : ∀ (UV : ↑s), EqOn (⇑(f UV)) (fun x => ε UV) (↑UV).2ᶜ<VAR>hf0ε : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 (ε UV)<VAR>hf01 : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 1<VAR>F : X → ↑s →ᵇ ℝ := fun x => { toFun := fun UV => (f UV) x, continuous_toFun := ⋯, map_bounded' := ⋯ }<GOAL>∃ f, Inducing f
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : SecondCountableTopology X<VAR>B : Set (Set X)<VAR>hBc : B.Countable<VAR>hB : IsTopologicalBasis B<VAR>s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure UV.1 ⊆ UV.2}<VAR>this✝¹ : Encodable ↑s<VAR>this✝ : TopologicalSpace ↑s := ⊥<VAR>this : DiscreteTopology ↑s<VAR>hd : ∀ (UV : ↑s), Disjoint (closure (↑UV).1) (↑UV).2ᶜ<VAR>ε : ↑s → ℝ<VAR>ε01 : ∀ (UV : ↑s), ε UV ∈ Ioc 0 1<VAR>hε : Tendsto ε cofinite (𝓝 0)<VAR>f : ↑s → C(X, ℝ)<VAR>hf0 : ∀ (UV : ↑s), EqOn (⇑(f UV)) 0 (↑UV).1<VAR>hfε : ∀ (UV : ↑s), EqOn (⇑(f UV)) (fun x => ε UV) (↑UV).2ᶜ<VAR>hf0ε : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 (ε UV)<VAR>hf01 : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 1<VAR>F : X → ↑s →ᵇ ℝ := fun x => { toFun := fun UV => (f UV) x, continuous_toFun := ⋯, map_bounded' := ⋯ }<VAR>hF : ∀ (x : X) (UV : ↑s), (F x) UV = (f UV) x<GOAL>∃ f, Inducing f
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : SecondCountableTopology X<VAR>B : Set (Set X)<VAR>hBc : B.Countable<VAR>hB : IsTopologicalBasis B<VAR>s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure UV.1 ⊆ UV.2}<VAR>this✝¹ : Encodable ↑s<VAR>this✝ : TopologicalSpace ↑s := ⊥<VAR>this : DiscreteTopology ↑s<VAR>hd : ∀ (UV : ↑s), Disjoint (closure (↑UV).1) (↑UV).2ᶜ<VAR>ε : ↑s → ℝ<VAR>ε01 : ∀ (UV : ↑s), ε UV ∈ Ioc 0 1<VAR>hε : Tendsto ε cofinite (𝓝 0)<VAR>f : ↑s → C(X, ℝ)<VAR>hf0 : ∀ (UV : ↑s), EqOn (⇑(f UV)) 0 (↑UV).1<VAR>hfε : ∀ (UV : ↑s), EqOn (⇑(f UV)) (fun x => ε UV) (↑UV).2ᶜ<VAR>hf0ε : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 (ε UV)<VAR>hf01 : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 1<VAR>F : X → ↑s →ᵇ ℝ := fun x => { toFun := fun UV => (f UV) x, continuous_toFun := ⋯, map_bounded' := ⋯ }<VAR>hF : ∀ (x : X) (UV : ↑s), (F x) UV = (f UV) x<VAR>x : X<GOAL>𝓝 x ≤ comap F (𝓝 (F x))
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : SecondCountableTopology X<VAR>B : Set (Set X)<VAR>hBc : B.Countable<VAR>hB : IsTopologicalBasis B<VAR>s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure UV.1 ⊆ UV.2}<VAR>this✝¹ : Encodable ↑s<VAR>this✝ : TopologicalSpace ↑s := ⊥<VAR>this : DiscreteTopology ↑s<VAR>hd : ∀ (UV : ↑s), Disjoint (closure (↑UV).1) (↑UV).2ᶜ<VAR>ε : ↑s → ℝ<VAR>ε01 : ∀ (UV : ↑s), ε UV ∈ Ioc 0 1<VAR>hε : Tendsto ε cofinite (𝓝 0)<VAR>f : ↑s → C(X, ℝ)<VAR>hf0 : ∀ (UV : ↑s), EqOn (⇑(f UV)) 0 (↑UV).1<VAR>hfε : ∀ (UV : ↑s), EqOn (⇑(f UV)) (fun x => ε UV) (↑UV).2ᶜ<VAR>hf0ε : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 (ε UV)<VAR>hf01 : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 1<VAR>F : X → ↑s →ᵇ ℝ := fun x => { toFun := fun UV => (f UV) x, continuous_toFun := ⋯, map_bounded' := ⋯ }<VAR>hF : ∀ (x : X) (UV : ↑s), (F x) UV = (f UV) x<VAR>x : X<GOAL>comap F (𝓝 (F x)) ≤ 𝓝 x
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hf : GrowsPolynomially f<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, c * f ↑n ≤ f u
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hf : GrowsPolynomially f<VAR>c : ℝ<VAR>hc_mem : c > 0<VAR>hc : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, c * f ↑n ≤ f u
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β✝ : Type u_3<VAR>γ✝ : Type u_4<VAR>κ : ι → Type u_5<VAR>β : Type u_6<VAR>β' : Type u_7<VAR>γ : Type u_8<VAR>γ' : Type u_9<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>IndepFun f g μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) μ
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>A : C<VAR>f g : A ⟶ X φ i<VAR>h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij<VAR>h₂ : f ≫ sndX φ i = g ≫ sndX φ i<GOAL>f = g
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>A : C<VAR>f g : A ⟶ X φ i<VAR>h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij<VAR>h₂ : f ≫ sndX φ i = g ≫ sndX φ i<VAR>this : HasBinaryBiproduct (F.X j) (G.X i)<GOAL>f = g
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>A : C<VAR>f g : A ⟶ X φ i<VAR>h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij<VAR>h₂ : f ≫ sndX φ i = g ≫ sndX φ i<VAR>this : HasBinaryBiproduct (F.X j) (G.X i)<GOAL>f ≫ (XIsoBiprod φ i j hij).hom = g ≫ (XIsoBiprod φ i j hij).hom
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>A : C<VAR>f g : A ⟶ X φ i<VAR>h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij<VAR>h₂ : f ≫ sndX φ i = g ≫ sndX φ i<VAR>this : HasBinaryBiproduct (F.X j) (G.X i)<GOAL>(f ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.fst = (g ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.fst
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>A : C<VAR>f g : A ⟶ X φ i<VAR>h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij<VAR>h₂ : f ≫ sndX φ i = g ≫ sndX φ i<VAR>this : HasBinaryBiproduct (F.X j) (G.X i)<GOAL>(f ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.snd = (g ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.snd
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>K : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝⁴ : Semifield K<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module K V<VAR>inst✝¹ : AddCommMonoid V₂<VAR>inst✝ : Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>p : Submodule K V<VAR>a : K<VAR>h : a ≠ 0<GOAL>map (a • f) p ≤ map f p
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>K : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝⁴ : Semifield K<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module K V<VAR>inst✝¹ : AddCommMonoid V₂<VAR>inst✝ : Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>p : Submodule K V<VAR>a : K<VAR>h : a ≠ 0<GOAL>map f p ≤ map (a • f) p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Fintype α<VAR>t : Finset β<VAR>hαt : Fintype.card α = t.card<VAR>s : Set α<VAR>f : α → β<VAR>hfst : MapsTo f s ↑t<VAR>hfs : InjOn f s<GOAL>∃ g, ∀ i ∈ s, ↑(g i) = f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Encodable β<VAR>inst✝ : CompleteLattice α<VAR>f : β → α<GOAL>⨆ i, ⨆ b ∈ decode₂ β i, f b = ⨆ b, f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Encodable β<VAR>inst✝ : CompleteLattice α<VAR>f : β → α<GOAL>⨆ j, ⨆ i, ⨆ (_ : j ∈ decode₂ β i), f j = ⨆ b, f b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>I : FractionalIdeal A⁰ K<VAR>hne : I ≠ 0<GOAL>I * I⁻¹ = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>I : FractionalIdeal A⁰ K<VAR>hne : I ≠ 0<VAR>a : A<VAR>J : Ideal A<VAR>ha : a ≠ 0<VAR>hJ : I = spanSingleton A⁰ ((algebraMap A K) a)⁻¹ * ↑J<GOAL>I * I⁻¹ = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>I : FractionalIdeal A⁰ K<VAR>hne : I ≠ 0<VAR>a : A<VAR>J : Ideal A<VAR>ha : a ≠ 0<VAR>hJ : I = spanSingleton A⁰ ((algebraMap A K) a)⁻¹ * ↑J<GOAL>I * (spanSingleton A⁰ ((algebraMap A K) a) * (↑J)⁻¹) = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>a : A<VAR>J : Ideal A<VAR>ha : a ≠ 0<VAR>hne : spanSingleton A⁰ ((algebraMap A K) a)⁻¹ * ↑J ≠ 0<GOAL>spanSingleton A⁰ ((algebraMap A K) a)⁻¹ * ↑J * (spanSingleton A⁰ ((algebraMap A K) a) * (↑J)⁻¹) = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>a : A<VAR>J : Ideal A<VAR>ha : a ≠ 0<VAR>hne : spanSingleton A⁰ ((algebraMap A K) a)⁻¹ * ↑J ≠ 0<GOAL>(algebraMap A K) a ≠ 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>a : A<VAR>J : Ideal A<VAR>ha : a ≠ 0<VAR>hne : spanSingleton A⁰ ((algebraMap A K) a)⁻¹ * ↑J ≠ 0<GOAL>J ≠ ⊥
<VAR>ι : Sort u_1<VAR>f✝ f : ι → ℝ≥0<VAR>a : ℝ≥0<GOAL>(⨆ i, f i) * a = ⨆ i, f i * a
<VAR>ι : Sort u_1<VAR>f✝ f : ι → ℝ≥0<VAR>a : ℝ≥0<GOAL>⨆ i, a * f i = ⨆ i, f i * a
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>U : Set M<VAR>hU : IsOpen U<VAR>hSig : IsSigmaCompact U<VAR>hf : LocallyIntegrableOn f U μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0<GOAL>∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>U : Set M<VAR>hU : IsOpen U<VAR>hSig : IsSigmaCompact U<VAR>hf : LocallyIntegrableOn f U μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0<VAR>meas_U : MeasurableSet U<GOAL>∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>U : Set M<VAR>hU : IsOpen U<VAR>hSig : IsSigmaCompact U<VAR>hf : LocallyIntegrableOn f U μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0<VAR>meas_U : MeasurableSet U<GOAL>∀ᵐ (x : ↑U) ∂Measure.comap Subtype.val μ, f ↑x = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>U✝ : Set M<VAR>hU : IsOpen U✝<VAR>hSig : IsSigmaCompact U✝<VAR>hf : LocallyIntegrableOn f U✝ μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → tsupport g ⊆ U✝ → ∫ (x : M), g x • f x ∂μ = 0<VAR>meas_U : MeasurableSet U✝<VAR>U : Opens M := { carrier := U✝, is_open' := hU }<GOAL>∀ᵐ (x : ↥U) ∂Measure.comap Subtype.val μ, f ↑x = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>U✝ : Set M<VAR>hU : IsOpen U✝<VAR>hSig : IsSigmaCompact U✝<VAR>hf : LocallyIntegrableOn f U✝ μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → tsupport g ⊆ U✝ → ∫ (x : M), g x • f x ∂μ = 0<VAR>meas_U : MeasurableSet U✝<VAR>U : Opens M := { carrier := U✝, is_open' := hU }<VAR>this : SigmaCompactSpace ↥U<GOAL>∀ᵐ (x : ↥U) ∂Measure.comap Subtype.val μ, f ↑x = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>U✝ : Set M<VAR>hU : IsOpen U✝<VAR>hSig : IsSigmaCompact U✝<VAR>hf : LocallyIntegrableOn f U✝ μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → tsupport g ⊆ U✝ → ∫ (x : M), g x • f x ∂μ = 0<VAR>meas_U : MeasurableSet U✝<VAR>U : Opens M := { carrier := U✝, is_open' := hU }<VAR>this : SigmaCompactSpace ↥U<GOAL>LocallyIntegrable (fun x => f ↑x) (Measure.comap Subtype.val μ)
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>U✝ : Set M<VAR>hU : IsOpen U✝<VAR>hSig : IsSigmaCompact U✝<VAR>hf : LocallyIntegrableOn f U✝ μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → tsupport g ⊆ U✝ → ∫ (x : M), g x • f x ∂μ = 0<VAR>meas_U : MeasurableSet U✝<VAR>U : Opens M := { carrier := U✝, is_open' := hU }<VAR>this : SigmaCompactSpace ↥U<VAR>g : ↥U → ℝ<VAR>g_smth : Smooth I 𝓘(ℝ, ℝ) g<VAR>g_supp : HasCompactSupport g<GOAL>∫ (x : ↥U), g x • f ↑x ∂Measure.comap Subtype.val μ = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>U✝ : Set M<VAR>hU : IsOpen U✝<VAR>hSig : IsSigmaCompact U✝<VAR>hf : LocallyIntegrableOn f U✝ μ<VAR>meas_U : MeasurableSet U✝<VAR>U : Opens M := { carrier := U✝, is_open' := hU }<VAR>this : SigmaCompactSpace ↥U<VAR>g : ↥U → ℝ<VAR>g_smth : Smooth I 𝓘(ℝ, ℝ) g<VAR>g_supp : HasCompactSupport g<VAR>h : ∫ (x : M), Function.extend Subtype.val g 0 x • f x ∂μ = 0<GOAL>∫ (x : ↥U), g x • f ↑x ∂Measure.comap Subtype.val μ = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>U✝ : Set M<VAR>hU : IsOpen U✝<VAR>hSig : IsSigmaCompact U✝<VAR>hf : LocallyIntegrableOn f U✝ μ<VAR>meas_U : MeasurableSet U✝<VAR>U : Opens M := { carrier := U✝, is_open' := hU }<VAR>this : SigmaCompactSpace ↥U<VAR>g : ↥U → ℝ<VAR>g_smth : Smooth I 𝓘(ℝ, ℝ) g<VAR>g_supp : HasCompactSupport g<VAR>h : ∫ (x : M) in ↑U, Function.extend Subtype.val g 0 x • f x ∂μ = 0<GOAL>∫ (x : ↥U), g x • f ↑x ∂Measure.comap Subtype.val μ = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>U✝ : Set M<VAR>hU : IsOpen U✝<VAR>hSig : IsSigmaCompact U✝<VAR>hf : LocallyIntegrableOn f U✝ μ<VAR>meas_U : MeasurableSet U✝<VAR>U : Opens M := { carrier := U✝, is_open' := hU }<VAR>this : SigmaCompactSpace ↥U<VAR>g : ↥U → ℝ<VAR>g_smth : Smooth I 𝓘(ℝ, ℝ) g<VAR>g_supp : HasCompactSupport g<VAR>h : ∫ (x : M), Function.extend Subtype.val g 0 x • f x ∂μ = 0<VAR>x : M<VAR>hx : x ∉ ↑U<GOAL>Function.extend Subtype.val g 0 x • f x = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>U✝ : Set M<VAR>hU : IsOpen U✝<VAR>hSig : IsSigmaCompact U✝<VAR>hf : LocallyIntegrableOn f U✝ μ<VAR>meas_U : MeasurableSet U✝<VAR>U : Opens M := { carrier := U✝, is_open' := hU }<VAR>this : SigmaCompactSpace ↥U<VAR>g : ↥U → ℝ<VAR>g_smth : Smooth I 𝓘(ℝ, ℝ) g<VAR>g_supp : HasCompactSupport g<VAR>h : ∫ (x : M), Function.extend Subtype.val g 0 x • f x ∂μ = 0<VAR>x : M<VAR>hx : x ∉ ↑U<GOAL>0 x • f x = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>U✝ : Set M<VAR>hU : IsOpen U✝<VAR>hSig : IsSigmaCompact U✝<VAR>hf : LocallyIntegrableOn f U✝ μ<VAR>meas_U : MeasurableSet U✝<VAR>U : Opens M := { carrier := U✝, is_open' := hU }<VAR>this : SigmaCompactSpace ↥U<VAR>g : ↥U → ℝ<VAR>g_smth : Smooth I 𝓘(ℝ, ℝ) g<VAR>g_supp : HasCompactSupport g<VAR>h : ∫ (x : M), Function.extend Subtype.val g 0 x • f x ∂μ = 0<VAR>x : M<VAR>hx : x ∉ ↑U<GOAL>(∃ a, ↑a = x) → x ∈ ↑U
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<GOAL>∀ {ι : Type u_1} [inst : _root_.Finite ι] (W : ι → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<GOAL>∀ {α β : Type u_1}, α ≃ β → (∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)) → ∀ (W : β → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<GOAL>∀ (W : PEmpty.{u_1 + 1} → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<GOAL>∀ {α : Type u_1} [inst : Fintype α], (∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)) → ∀ (W : Option α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter β<VAR>m : α → β<VAR>hf : f.NeBot<VAR>s : Set α<VAR>hs : m '' s ∈ f<GOAL>(comap m f ⊓ 𝓟 s).NeBot