ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → MeasureTheory.Measure (α i)<VAR>β : ι → Type u_4<VAR>(i : ι) → MeasurableSpace (β i)<VAR>ν : (i : ι) → MeasureTheory.Measure (β i)<VAR>f : (i : ι) → α i → β i<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (ν i)<VAR>hf : ∀ (i : ι), MeasureTheory.MeasurePreserving (f i) (μ i) (ν i)<GOAL>MeasureTheory.MeasurePreserving (fun a i => f i (a i)) (MeasureTheory.Measure.pi μ) (MeasureTheory.Measure.pi ν)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>α' : ι → Type u_4<VAR>β' : ι → Type u_5<VAR>(i : ι) → MeasureTheory.MeasureSpace (α' i)<VAR>(i : ι) → MeasureTheory.MeasureSpace (β' i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume<VAR>f : (i : ι) → α' i → β' i<VAR>hf : ∀ (i : ι), MeasureTheory.MeasurePreserving (f i) MeasureTheory.volume MeasureTheory.volume<GOAL>MeasureTheory.MeasurePreserving (fun a i => f i (a i)) MeasureTheory.volume MeasureTheory.volume
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>self : StandardBorelSpace α<GOAL>∃ x, BorelSpace α ∧ PolishSpace α
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>StandardBorelSpace α<GOAL>inst✝ = borel α
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>MeasureTheory.AnalyticSet s = (s = ∅ ∨ ∃ f, Continuous f ∧ Set.range f = s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>MeasureTheory.AnalyticSet ∅
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>PolishSpace β<VAR>f : β → α<VAR>f_cont : Continuous f<GOAL>MeasureTheory.AnalyticSet (Set.range f)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>PolishSpace β<VAR>s : Set β<VAR>hs : IsOpen s<VAR>f : β → α<VAR>f_cont : Continuous f<GOAL>MeasureTheory.AnalyticSet (f '' s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>MeasureTheory.AnalyticSet s ↔ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ Set.range f = s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>s : Set α<VAR>hs : MeasureTheory.AnalyticSet s<VAR>f : α → β<VAR>hf : ContinuousOn f s<GOAL>MeasureTheory.AnalyticSet (f '' s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>s : Set α<VAR>hs : MeasureTheory.AnalyticSet s<VAR>f : α → β<VAR>hf : Continuous f<GOAL>MeasureTheory.AnalyticSet (f '' s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>TopologicalSpace α<VAR>hι : Nonempty ι<VAR>Countable ι<VAR>T2Space α<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), MeasureTheory.AnalyticSet (s n)<GOAL>MeasureTheory.AnalyticSet (⋂ n, s n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>TopologicalSpace α<VAR>Countable ι<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), MeasureTheory.AnalyticSet (s n)<GOAL>MeasureTheory.AnalyticSet (⋃ n, s n)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>PolishSpace α<VAR>s : Set α<VAR>hs : IsClosed s<GOAL>MeasureTheory.AnalyticSet s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>PolishSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>PolishSpace.IsClopenable s
<VAR>α : Type u_3<VAR>t : TopologicalSpace α<VAR>PolishSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.AnalyticSet s
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>t : TopologicalSpace α<VAR>PolishSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>tβ : TopologicalSpace β<VAR>MeasurableSpace β<VAR>OpensMeasurableSpace β<VAR>f : α → β<VAR>SecondCountableTopology ↑(Set.range f)<VAR>hf : Measurable f<GOAL>∃ t' ≤ t, Continuous f ∧ PolishSpace α
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>MeasurableSpace X<VAR>StandardBorelSpace X<VAR>TopologicalSpace Y<VAR>MeasurableSpace Y<VAR>OpensMeasurableSpace Y<VAR>f : X → Y<VAR>SecondCountableTopology ↑(Set.range f)<VAR>s : Set X<VAR>hs : MeasurableSet s<VAR>hf : Measurable f<GOAL>MeasureTheory.AnalyticSet (f '' s)
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>PolishSpace X<VAR>T2Space Y<VAR>s : Set Y<VAR>hs : MeasureTheory.AnalyticSet s<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>MeasureTheory.AnalyticSet (f ⁻¹' s)
<VAR>ι : Type u_2<VAR>Countable ι<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>s t : ι → Set α<VAR>h : ∀ (m n : ι), MeasureTheory.MeasurablySeparable (s m) (t n)<GOAL>MeasureTheory.MeasurablySeparable (⋃ n, s n) (⋃ m, t m)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>T2Space α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>f g : (ℕ → ℕ) → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : Disjoint (Set.range f) (Set.range g)<GOAL>MeasureTheory.MeasurablySeparable (Set.range f) (Set.range g)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>T2Space α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>s t : Set α<VAR>hs : MeasureTheory.AnalyticSet s<VAR>ht : MeasureTheory.AnalyticSet t<VAR>h : Disjoint s t<GOAL>MeasureTheory.MeasurablySeparable s t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>T2Space α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>s : Set α<VAR>hs : MeasureTheory.AnalyticSet s<VAR>hsc : MeasureTheory.AnalyticSet sᶜ<GOAL>MeasurableSet s
<VAR>X : Type u_3<VAR>Z : Type u_5<VAR>MeasurableSpace X<VAR>StandardBorelSpace X<VAR>MeasurableSpace Z<VAR>MeasurableSpace.CountablySeparated Z<VAR>f : X → Z<VAR>hf : Measurable f<VAR>hsurj : Function.Surjective f<VAR>s : Set Z<GOAL>MeasurableSet (f ⁻¹' s) ↔ MeasurableSet s
<VAR>X : Type u_3<VAR>Z : Type u_5<VAR>MeasurableSpace X<VAR>StandardBorelSpace X<VAR>MeasurableSpace Z<VAR>MeasurableSpace.CountablySeparated Z<VAR>f : X → Z<VAR>hf : Measurable f<VAR>hsurj : Function.Surjective f<GOAL>MeasurableSpace.map f inst✝ = inst✝¹
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>MeasurableSpace X<VAR>StandardBorelSpace X<VAR>TopologicalSpace Y<VAR>T0Space Y<VAR>MeasurableSpace Y<VAR>OpensMeasurableSpace Y<VAR>SecondCountableTopology Y<VAR>f : X → Y<VAR>hf : Measurable f<VAR>hsurj : Function.Surjective f<GOAL>MeasurableSpace.map f inst✝ = borel Y
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>MeasurableSpace X<VAR>StandardBorelSpace X<VAR>TopologicalSpace Y<VAR>T0Space Y<VAR>MeasurableSpace Y<VAR>OpensMeasurableSpace Y<VAR>SecondCountableTopology Y<VAR>f : X → Y<VAR>hf : Measurable f<VAR>hsurj : Function.Surjective f<GOAL>BorelSpace Y
<VAR>X : Type u_3<VAR>Z : Type u_5<VAR>MeasurableSpace X<VAR>StandardBorelSpace X<VAR>MeasurableSpace Z<VAR>f : X → Z<VAR>MeasurableSpace.CountablySeparated ↑(Set.range f)<VAR>hf : Measurable f<VAR>s : Set Z<GOAL>MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (Subtype.val ⁻¹' s)
<VAR>X : Type u_3<VAR>Z : Type u_5<VAR>MeasurableSpace X<VAR>StandardBorelSpace X<VAR>MeasurableSpace Z<VAR>f : X → Z<VAR>MeasurableSpace.CountablySeparated ↑(Set.range f)<VAR>hf : Measurable f<VAR>hr : MeasurableSet (Set.range f)<VAR>s : Set Z<GOAL>MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ Set.range f)
<VAR>X : Type u_3<VAR>Z : Type u_5<VAR>β : Type u_6<VAR>MeasurableSpace X<VAR>StandardBorelSpace X<VAR>MeasurableSpace β<VAR>MeasurableSpace Z<VAR>f : X → Z<VAR>MeasurableSpace.CountablySeparated ↑(Set.range f)<VAR>hf : Measurable f<VAR>g : Z → β<GOAL>Measurable (g ∘ f) ↔ Measurable ((Set.range f).restrict g)
<VAR>X : Type u_3<VAR>Z : Type u_5<VAR>β : Type u_6<VAR>MeasurableSpace X<VAR>StandardBorelSpace X<VAR>MeasurableSpace β<VAR>MeasurableSpace Z<VAR>MeasurableSpace.CountablySeparated Z<VAR>f : X → Z<VAR>hf : Measurable f<VAR>hsurj : Function.Surjective f<VAR>g : Z → β<GOAL>Measurable (g ∘ f) ↔ Measurable g
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>PolishSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>TopologicalSpace Y<VAR>T0Space Y<VAR>SecondCountableTopology Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>hsurj : Function.Surjective f<GOAL>MeasurableSpace.map f inst✝ = borel Y
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>PolishSpace X<VAR>TopologicalSpace Y<VAR>T0Space Y<VAR>SecondCountableTopology Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>hsurj : Function.Surjective f<GOAL>MeasurableSpace.map f (borel X) = borel Y
<VAR>γ : Type u_3<VAR>β : Type u_4<VAR>TopologicalSpace γ<VAR>PolishSpace γ<VAR>TopologicalSpace β<VAR>T2Space β<VAR>MeasurableSpace β<VAR>OpensMeasurableSpace β<VAR>f : γ → β<VAR>f_cont : Continuous f<VAR>f_inj : Function.Injective f<GOAL>MeasurableSet (Set.range f)
<VAR>γ : Type u_3<VAR>TopologicalSpace γ<VAR>PolishSpace γ<VAR>β : Type u_4<VAR>TopologicalSpace β<VAR>T2Space β<VAR>MeasurableSpace β<VAR>OpensMeasurableSpace β<VAR>s : Set γ<VAR>hs : IsClosed s<VAR>f : γ → β<VAR>f_cont : ContinuousOn f s<VAR>f_inj : Set.InjOn f s<GOAL>MeasurableSet (f '' s)
<VAR>γ : Type u_3<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>T2Space β<VAR>MeasurableSpace β<VAR>s : Set γ<VAR>f : γ → β<VAR>OpensMeasurableSpace β<VAR>tγ : TopologicalSpace γ<VAR>PolishSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>hs : MeasurableSet s<VAR>f_cont : ContinuousOn f s<VAR>f_inj : Set.InjOn f s<GOAL>MeasurableSet (f '' s)
<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace α<VAR>s : Set γ<VAR>f : γ → α<VAR>MeasurableSpace.CountablySeparated α<VAR>MeasurableSpace γ<VAR>StandardBorelSpace γ<VAR>hs : MeasurableSet s<VAR>f_meas : Measurable f<VAR>f_inj : Set.InjOn f s<GOAL>MeasurableSet (f '' s)
<VAR>γ : Type u_3<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>T2Space β<VAR>MeasurableSpace β<VAR>f : γ → β<VAR>BorelSpace β<VAR>TopologicalSpace γ<VAR>PolishSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>f_cont : Continuous f<VAR>f_inj : Function.Injective f<GOAL>MeasurableEmbedding f
<VAR>γ : Type u_3<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>T2Space β<VAR>MeasurableSpace β<VAR>s : Set γ<VAR>f : γ → β<VAR>BorelSpace β<VAR>TopologicalSpace γ<VAR>PolishSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>hs : MeasurableSet s<VAR>f_cont : ContinuousOn f s<VAR>f_inj : Set.InjOn f s<GOAL>MeasurableEmbedding (s.restrict f)
<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace α<VAR>f : γ → α<VAR>MeasurableSpace.CountablySeparated α<VAR>MeasurableSpace γ<VAR>StandardBorelSpace γ<VAR>f_meas : Measurable f<VAR>f_inj : Function.Injective f<GOAL>MeasurableEmbedding f
<VAR>γ : Type u_3<VAR>t t' : TopologicalSpace γ<VAR>ht : PolishSpace γ<VAR>ht' : PolishSpace γ<VAR>hle : t ≤ t'<GOAL>borel γ = borel γ
<VAR>γ : Type u_3<VAR>s : Set γ<VAR>tγ : TopologicalSpace γ<VAR>PolishSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<GOAL>PolishSpace.IsClopenable s ↔ MeasurableSet s
<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>β : Type u_5<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>Countable ι<VAR>l : Filter ι<VAR>l.IsCountablyGenerated<VAR>TopologicalSpace γ<VAR>SecondCountableTopology γ<VAR>TopologicalSpace.PseudoMetrizableSpace γ<VAR>OpensMeasurableSpace γ<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>g : β → γ<VAR>hg : Measurable g<GOAL>MeasurableSet {x | Filter.Tendsto (fun n => f n x) l (𝓝 (g x))}
<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>β : Type u_5<VAR>MeasurableSpace β<VAR>TopologicalSpace γ<VAR>PolishSpace γ<VAR>MeasurableSpace γ<VAR>hγ : OpensMeasurableSpace γ<VAR>Countable ι<VAR>l : Filter ι<VAR>l.IsCountablyGenerated<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<GOAL>MeasurableSet {x | ∃ c, Filter.Tendsto (fun n => f n x) l (𝓝 c)}
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>StandardBorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∃ x, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>StandardBorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>StandardBorelSpace ↑s
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>∀ {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : OpensMeasurableSpace E] [inst_2 : SecondCountableTopology E] {f g : α → E}, Measurable f → Measurable g → Measurable fun t => ⟪f t, g t⟫_𝕜
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>∀ {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : OpensMeasurableSpace E] [inst_2 : SecondCountableTopology E] {c : E} {f : α → E}, Measurable f → Measurable fun t => ⟪c, f t⟫_𝕜
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>∀ {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : OpensMeasurableSpace E] [inst_2 : SecondCountableTopology E] {c : E} {f : α → E}, Measurable f → Measurable fun t => ⟪f t, c⟫_𝕜
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>m : MeasurableSpace α<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>SecondCountableTopology E<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun x => ⟪f x, g x⟫_𝕜) μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>m : MeasurableSpace α<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>SecondCountableTopology E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>c : E<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => ⟪c, f x⟫_𝕜) μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>m : MeasurableSpace α<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>SecondCountableTopology E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>c : E<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => ⟪f x, c⟫_𝕜) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ<VAR>hf : Measurable f<GOAL>Measurable fun x => Real.arctan (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>MetricSpace β<VAR>n : ℕ<VAR>j : ι<VAR>f : ι → α → β<VAR>g : α → β<VAR>Preorder ι<VAR>x : α<GOAL>x ∈ MeasureTheory.Egorov.notConvergentSeq f g n j ↔ ∃ k ≥ j, 1 / (↑n + 1) < dist (f k x) (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>MetricSpace β<VAR>n : ℕ<VAR>f : ι → α → β<VAR>g : α → β<VAR>Preorder ι<GOAL>Antitone (MeasureTheory.Egorov.notConvergentSeq f g n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>MetricSpace β<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : ι → α → β<VAR>g : α → β<VAR>SemilatticeSup ι<VAR>Nonempty ι<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<VAR>n : ℕ<GOAL>μ (s ∩ ⋂ j, MeasureTheory.Egorov.notConvergentSeq f g n j) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>MetricSpace β<VAR>n : ℕ<VAR>j : ι<VAR>f : ι → α → β<VAR>g : α → β<VAR>Preorder ι<VAR>Countable ι<VAR>hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>MeasurableSet (MeasureTheory.Egorov.notConvergentSeq f g n j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>MetricSpace β<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : ι → α → β<VAR>g : α → β<VAR>SemilatticeSup ι<VAR>Countable ι<VAR>hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<VAR>n : ℕ<GOAL>Filter.Tendsto (fun j => μ (s ∩ MeasureTheory.Egorov.notConvergentSeq f g n j)) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>MetricSpace β<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>SemilatticeSup ι<VAR>Nonempty ι<VAR>Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<VAR>n : ℕ<GOAL>∃ j, μ (s ∩ MeasureTheory.Egorov.notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>MetricSpace β<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>SemilatticeSup ι<VAR>Nonempty ι<VAR>Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<VAR>n : ℕ<GOAL>μ (s ∩ MeasureTheory.Egorov.notConvergentSeq f g n (MeasureTheory.Egorov.notConvergentSeqLTIndex hε hf hg hsm hs hfg n)) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>MetricSpace β<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>SemilatticeSup ι<VAR>Nonempty ι<VAR>Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<GOAL>MeasurableSet (MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hg hsm hs hfg)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>MetricSpace β<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>SemilatticeSup ι<VAR>Nonempty ι<VAR>Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<GOAL>μ (MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hg hsm hs hfg) ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>MetricSpace β<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>SemilatticeSup ι<VAR>Nonempty ι<VAR>Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<GOAL>MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hg hsm hs hfg ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>MetricSpace β<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>SemilatticeSup ι<VAR>Nonempty ι<VAR>Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<GOAL>TendstoUniformlyOn f g Filter.atTop (s \ MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hg hsm hs hfg)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>MetricSpace β<VAR>μ : MeasureTheory.Measure α<VAR>SemilatticeSup ι<VAR>Nonempty ι<VAR>Countable ι<VAR>f : ι → α → β<VAR>g : α → β<VAR>s : Set α<VAR>hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ t ⊆ s, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g Filter.atTop (s \ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>MetricSpace β<VAR>μ : MeasureTheory.Measure α<VAR>SemilatticeSup ι<VAR>Nonempty ι<VAR>Countable ι<VAR>f : ι → α → β<VAR>g : α → β<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ t, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g Filter.atTop tᶜ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>SeminormedAddCommGroup E<VAR>l : Filter ι<VAR>f : ι → α → E<VAR>g : α → E<GOAL>MeasureTheory.TendstoInMeasure μ f l g ↔ ∀ (ε : ℝ), 0 < ε → Filter.Tendsto (fun i => μ {x | ε ≤ ‖f i x - g x‖}) l (𝓝 0)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Dist E<VAR>l : Filter ι<VAR>f f' : ι → α → E<VAR>g g' : α → E<VAR>h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i<VAR>h_right : g =ᵐ[μ] g'<VAR>h_tendsto : MeasureTheory.TendstoInMeasure μ f l g<GOAL>MeasureTheory.TendstoInMeasure μ f' l g'
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Dist E<VAR>l : Filter ι<VAR>f f' : ι → α → E<VAR>g g' : α → E<VAR>h_left : ∀ (i : ι), f i =ᵐ[μ] f' i<VAR>h_right : g =ᵐ[μ] g'<VAR>h_tendsto : MeasureTheory.TendstoInMeasure μ f l g<GOAL>MeasureTheory.TendstoInMeasure μ f' l g'
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Dist E<VAR>l : Filter ι<VAR>f f' : ι → α → E<VAR>g : α → E<VAR>h : ∀ (i : ι), f i =ᵐ[μ] f' i<VAR>h_tendsto : MeasureTheory.TendstoInMeasure μ f l g<GOAL>MeasureTheory.TendstoInMeasure μ f' l g
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Dist E<VAR>l : Filter ι<VAR>f : ι → α → E<VAR>g g' : α → E<VAR>h : g =ᵐ[μ] g'<VAR>h_tendsto : MeasureTheory.TendstoInMeasure μ f l g<GOAL>MeasureTheory.TendstoInMeasure μ f l g'
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (f n)<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<GOAL>MeasureTheory.TendstoInMeasure μ f Filter.atTop g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<GOAL>MeasureTheory.TendstoInMeasure μ f Filter.atTop g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g<VAR>n : ℕ<GOAL>∃ N, ∀ m_1 ≥ N, μ {x | 2⁻¹ ^ n ≤ dist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g<VAR>n : ℕ<GOAL>MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg (n + 1) = max (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux hfg (n + 1)) (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg n + 1)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g<VAR>n k : ℕ<VAR>hn : MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg n ≤ k<GOAL>μ {x | 2⁻¹ ^ n ≤ dist (f k x) (g x)} ≤ 2⁻¹ ^ n
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g<GOAL>StrictMono (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g<GOAL>∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun i => f (ns i) x) Filter.atTop (𝓝 (g x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MetricSpace E<VAR>u : Filter ι<VAR>u.NeBot<VAR>u.IsCountablyGenerated<VAR>f : ι → α → E<VAR>g : α → E<VAR>hfg : MeasureTheory.TendstoInMeasure μ f u g<GOAL>∃ ns, MeasureTheory.TendstoInMeasure μ (fun n => f (ns n)) Filter.atTop g