ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LinearOrder X<VAR>OrderTopology X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>DenselyOrdered X<VAR>a b : X<GOAL>μ (Set.Ioo a b) = 0 ↔ b ≤ a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>LinearOrder X<VAR>OrderTopology X<VAR>m : MeasurableSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>a b : X<VAR>f g : X → Y<VAR>hfg : f =ᵐ[μ.restrict (Set.Ioo a b)] g<VAR>hf : ContinuousOn f (Set.Ioo a b)<VAR>hg : ContinuousOn g (Set.Ioo a b)<GOAL>Set.EqOn f g (Set.Ioo a b)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>LinearOrder X<VAR>OrderTopology X<VAR>m : MeasurableSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>DenselyOrdered X<VAR>a b : X<VAR>f g : X → Y<VAR>hfg : f =ᵐ[μ.restrict (Set.Ioc a b)] g<VAR>hf : ContinuousOn f (Set.Ioc a b)<VAR>hg : ContinuousOn g (Set.Ioc a b)<GOAL>Set.EqOn f g (Set.Ioc a b)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>LinearOrder X<VAR>OrderTopology X<VAR>m : MeasurableSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>DenselyOrdered X<VAR>a b : X<VAR>f g : X → Y<VAR>hfg : f =ᵐ[μ.restrict (Set.Ico a b)] g<VAR>hf : ContinuousOn f (Set.Ico a b)<VAR>hg : ContinuousOn g (Set.Ico a b)<GOAL>Set.EqOn f g (Set.Ico a b)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>LinearOrder X<VAR>OrderTopology X<VAR>m : MeasurableSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>DenselyOrdered X<VAR>a b : X<VAR>hne : a ≠ b<VAR>f g : X → Y<VAR>hfg : f =ᵐ[μ.restrict (Set.Icc a b)] g<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hg : ContinuousOn g (Set.Icc a b)<GOAL>Set.EqOn f g (Set.Icc a b)
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>x : X<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>0 < μ (Metric.ball x r)
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>x : X<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>0 < μ (Metric.closedBall x r)
<VAR>X : Type u_2<VAR>MetricSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>MeasureTheory.NoAtoms μ<VAR>x : X<VAR>r : ℝ<GOAL>0 < μ (Metric.closedBall x r) ↔ 0 < r
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>x : X<VAR>r : ℝ≥0∞<VAR>hr : r ≠ 0<GOAL>0 < μ (EMetric.ball x r)
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<VAR>m : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>x : X<VAR>r : ℝ≥0∞<VAR>hr : r ≠ 0<GOAL>0 < μ (EMetric.closedBall x r)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>h₁s : IsClosed s<VAR>h₂s : μ s = 0<GOAL>IsNowhereDense s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>T2Space X<VAR>h₁s : IsSigmaCompact s<VAR>h₂s : μ s = 0<GOAL>IsMeagre s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompletelyRegularSpace X<VAR>K : Set X<VAR>K_closed : IsClosed K<VAR>x : X<VAR>x_notin_K : x ∉ K<GOAL>∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0
<VAR>X : Type u_2<VAR>MeasurableSpace X<VAR>MeasurableSpace.SeparatesPoints X<GOAL>Function.Injective fun x => MeasureTheory.diracProba x
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>x : X<VAR>A : Set X<VAR>A_mble : MeasurableSet A<GOAL>↑(MeasureTheory.diracProba x) A = A.indicator 1 x
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>x : X<VAR>A : Set X<VAR>x_in_A : x ∈ A<GOAL>↑(MeasureTheory.diracProba x) A = 1
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>MeasurableSingletonClass X<VAR>x : X<VAR>A : Set X<GOAL>↑(MeasureTheory.diracProba x) A = A.indicator 1 x
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<GOAL>Continuous fun x => MeasureTheory.diracProba x
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>T0Space X<GOAL>Function.Injective fun x => MeasureTheory.diracProba x
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>CompletelyRegularSpace X<VAR>x : X<VAR>L : Filter X<VAR>h : ¬Filter.Tendsto id L (𝓝 x)<GOAL>¬Filter.Tendsto MeasureTheory.diracProba L (𝓝 (MeasureTheory.diracProba x))
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>CompletelyRegularSpace X<VAR>x : X<VAR>L : Filter X<GOAL>Filter.Tendsto MeasureTheory.diracProba L (𝓝 (MeasureTheory.diracProba x)) ↔ Filter.Tendsto id L (𝓝 x)
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : ↑(Set.range MeasureTheory.diracProba)<GOAL>MeasureTheory.diracProba (MeasureTheory.diracProbaInverse μ) = ↑μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>T0Space X<VAR>x : X<VAR>μ : ↑(Set.range MeasureTheory.diracProba)<VAR>h : ↑μ = MeasureTheory.diracProba x<GOAL>MeasureTheory.diracProbaInverse μ = x
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>T0Space X<GOAL>MeasureTheory.diracProba ∘ ⇑MeasureTheory.diracProbaEquiv.symm = fun μ => ↑μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>T0Space X<VAR>CompletelyRegularSpace X<VAR>μ : ↑(Set.range MeasureTheory.diracProba)<VAR>F : Filter ↑(Set.range MeasureTheory.diracProba)<GOAL>Filter.Tendsto (⇑MeasureTheory.diracProbaEquiv.symm) F (𝓝 (MeasureTheory.diracProbaEquiv.symm μ)) ↔ Filter.Tendsto id F (𝓝 μ)
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>T0Space X<GOAL>Continuous ⇑MeasureTheory.diracProbaEquiv
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>T0Space X<VAR>CompletelyRegularSpace X<GOAL>Continuous ⇑MeasureTheory.diracProbaEquiv.symm
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<VAR>CompletelyRegularSpace X<VAR>MeasurableSpace X<VAR>OpensMeasurableSpace X<GOAL>Embedding fun x => MeasureTheory.diracProba x
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : MeasurableSet s<GOAL>MeasureTheory.NullMeasurableSet s μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.NullMeasurableSet ∅ μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.NullMeasurableSet Set.univ μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : μ s = 0<GOAL>MeasureTheory.NullMeasurableSet s μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : MeasureTheory.NullMeasurableSet s μ<GOAL>MeasureTheory.NullMeasurableSet sᶜ μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : MeasureTheory.NullMeasurableSet sᶜ μ<GOAL>MeasureTheory.NullMeasurableSet s μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>MeasureTheory.NullMeasurableSet sᶜ μ ↔ MeasureTheory.NullMeasurableSet s μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>Subsingleton α<GOAL>MeasureTheory.NullMeasurableSet s μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>h : s =ᵐ[μ] t<GOAL>MeasureTheory.NullMeasurableSet t μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Sort u_5<VAR>Countable ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ<GOAL>MeasureTheory.NullMeasurableSet (⋃ i, s i) μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ι → Set α<VAR>s : Set ι<VAR>hs : s.Countable<VAR>h : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ<GOAL>MeasureTheory.NullMeasurableSet (⋃ b ∈ s, f b) μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set (Set α)<VAR>hs : s.Countable<VAR>h : ∀ t ∈ s, MeasureTheory.NullMeasurableSet t μ<GOAL>MeasureTheory.NullMeasurableSet (⋃₀ s) μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Sort u_5<VAR>Countable ι<VAR>f : ι → Set α<VAR>h : ∀ (i : ι), MeasureTheory.NullMeasurableSet (f i) μ<GOAL>MeasureTheory.NullMeasurableSet (⋂ i, f i) μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : β → Set α<VAR>s : Set β<VAR>hs : s.Countable<VAR>h : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ<GOAL>MeasureTheory.NullMeasurableSet (⋂ b ∈ s, f b) μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set (Set α)<VAR>hs : s.Countable<VAR>h : ∀ t ∈ s, MeasureTheory.NullMeasurableSet t μ<GOAL>MeasureTheory.NullMeasurableSet (⋂₀ s) μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>ht : MeasureTheory.NullMeasurableSet t μ<GOAL>MeasureTheory.NullMeasurableSet (s ∪ t) μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>ht : μ t = 0<GOAL>MeasureTheory.NullMeasurableSet (s ∪ t) μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>ht : MeasureTheory.NullMeasurableSet t μ<GOAL>MeasureTheory.NullMeasurableSet (s ∩ t) μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>ht : MeasureTheory.NullMeasurableSet t μ<GOAL>MeasureTheory.NullMeasurableSet (s \ t) μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → Set α<VAR>h : ∀ (i : ℕ), MeasureTheory.NullMeasurableSet (f i) μ<VAR>n : ℕ<GOAL>MeasureTheory.NullMeasurableSet (disjointed f n) μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : Prop<GOAL>MeasureTheory.NullMeasurableSet {_a | p} μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>a : α<GOAL>MeasureTheory.NullMeasurableSet (insert a s) μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : MeasureTheory.NullMeasurableSet s μ<GOAL>∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : MeasureTheory.NullMeasurableSet s μ<GOAL>MeasureTheory.toMeasurable μ s =ᵐ[μ] s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : MeasureTheory.NullMeasurableSet s μ<GOAL>(MeasureTheory.toMeasurable μ sᶜ)ᶜ =ᵐ[μ] s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : MeasureTheory.NullMeasurableSet s μ<GOAL>∃ t ⊆ s, MeasurableSet t ∧ t =ᵐ[μ] s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ<VAR>hd : Pairwise (MeasureTheory.AEDisjoint μ on s)<GOAL>∃ t, (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᵐ[μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>f : ι → Set α<VAR>hn : Pairwise (Disjoint on f)<VAR>h : ∀ (i : ι), MeasurableSet (f i)<GOAL>μ (⋃ i, f i) = ∑' (i : ι), μ (f i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable ι<VAR>f : ι → Set α<VAR>hd : Pairwise (MeasureTheory.AEDisjoint μ on f)<VAR>h : ∀ (i : ι), MeasureTheory.NullMeasurableSet (f i) μ<GOAL>μ (⋃ i, f i) = ∑' (i : ι), μ (f i)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>ht : MeasureTheory.NullMeasurableSet t μ<VAR>hd : MeasureTheory.AEDisjoint μ s t<GOAL>μ (s ∪ t) = μ s + μ t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : Set α<VAR>s : Set α<VAR>ht : MeasureTheory.NullMeasurableSet t μ<GOAL>μ (s ∩ t) + μ (s \ t) = μ s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : Set α<VAR>s : Set α<VAR>ht : MeasureTheory.NullMeasurableSet t μ<GOAL>μ (s ∪ t) + μ (s ∩ t) = μ s + μ t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>t : Set α<GOAL>μ (s ∪ t) + μ (s ∩ t) = μ s + μ t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>ht : MeasureTheory.NullMeasurableSet t μ<VAR>hd : MeasureTheory.AEDisjoint μ s t<GOAL>μ (s ∪ t) = μ s + μ t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>hd : MeasureTheory.AEDisjoint μ s t<GOAL>μ (s ∪ t) = μ s + μ t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>μ s + μ sᶜ = μ Set.univ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)<VAR>x : α<GOAL>MeasureTheory.NullMeasurableSet {x} μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)<VAR>a : α<VAR>s : Set α<GOAL>MeasureTheory.NullMeasurableSet (insert a s) μ ↔ MeasureTheory.NullMeasurableSet s μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)<VAR>a : α<GOAL>MeasureTheory.NullMeasurableSet {x | x = a} μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)<VAR>hs : s.Finite<GOAL>MeasureTheory.NullMeasurableSet s μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)<VAR>s : Finset α<GOAL>MeasureTheory.NullMeasurableSet (↑s) μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ι → Set α<VAR>s : Set ι<VAR>hs : s.Finite<VAR>h : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ<GOAL>MeasureTheory.NullMeasurableSet (⋃ b ∈ s, f b) μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ι → Set α<VAR>s : Finset ι<VAR>h : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ<GOAL>MeasureTheory.NullMeasurableSet (⋃ b ∈ s, f b) μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set (Set α)<VAR>hs : s.Finite<VAR>h : ∀ t ∈ s, MeasureTheory.NullMeasurableSet t μ<GOAL>MeasureTheory.NullMeasurableSet (⋃₀ s) μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ι → Set α<VAR>s : Set ι<VAR>hs : s.Finite<VAR>h : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ<GOAL>MeasureTheory.NullMeasurableSet (⋂ b ∈ s, f b) μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ι → Set α<VAR>s : Finset ι<VAR>h : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ<GOAL>MeasureTheory.NullMeasurableSet (⋂ b ∈ s, f b) μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set (Set α)<VAR>hs : s.Finite<VAR>h : ∀ t ∈ s, MeasureTheory.NullMeasurableSet t μ<GOAL>MeasureTheory.NullMeasurableSet (⋂₀ s) μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>MeasureTheory.NullMeasurableSet (MeasureTheory.toMeasurable μ s) μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>h : Measurable f<GOAL>MeasureTheory.NullMeasurable f μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.NullMeasurable f μ<GOAL>Measurable f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>g : β → γ<VAR>hg : Measurable g<VAR>hf : MeasureTheory.NullMeasurable f μ<GOAL>MeasureTheory.NullMeasurable (g ∘ f) μ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>g : α → β<VAR>hf : MeasureTheory.NullMeasurable f μ<VAR>hg : f =ᵐ[μ] g<GOAL>MeasureTheory.NullMeasurable g μ
<VAR>α : Type u_2<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : μ.IsComplete] (s : Set α), μ s = 0 → MeasurableSet s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.IsComplete ↔ ∀ (s : Set α), μ s = 0 → MeasurableSet s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>h : μ.IsComplete<VAR>s : Set α<GOAL>μ s = 0 → MeasurableSet s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>μ.IsComplete<VAR>hs : μ s = 0<GOAL>MeasurableSet s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>μ.IsComplete<GOAL>MeasurableSet s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.IsComplete<VAR>_m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasureTheory.NullMeasurable f μ<GOAL>Measurable f
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>_hμ : μ.IsComplete<VAR>f g : α → β<VAR>hf : Measurable f<VAR>hfg : f =ᵐ[μ] g<GOAL>Measurable g
<VAR>α : Type u_2<GOAL>∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α), ⇑μ.completion = ⇑μ
<VAR>α : Type u_2<GOAL>∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α), μ.completion s = μ s
<VAR>α : Type u_2<GOAL>∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α), MeasureTheory.ae μ.completion = MeasureTheory.ae μ
<VAR>α : Type u_5<VAR>β : Type u_6<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] {f : α → β} {μ : MeasureTheory.Measure α}, MeasureTheory.StronglyMeasurable f → MeasureTheory.AEStronglyMeasurable f μ
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>Subsingleton β<VAR>f : α → β<GOAL>MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_5<VAR>β : Type u_6<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] (f : MeasureTheory.SimpleFunc α β), MeasureTheory.StronglyMeasurable ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite α<GOAL>∀ {x : MeasurableSpace α} [inst : MeasurableSingletonClass α] [inst : TopologicalSpace β] (f : α → β), MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>IsEmpty α<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] (f : α → β), MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_5<VAR>β : Type u_6<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] {b : β}, MeasureTheory.StronglyMeasurable fun x => b
<VAR>α : Type u_5<VAR>β : Type u_6<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Zero β], MeasureTheory.StronglyMeasurable 0
<VAR>α : Type u_5<VAR>β : Type u_6<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : One β], MeasureTheory.StronglyMeasurable 1
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>m : MeasurableSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : ∀ (x y : α), f x = f y<GOAL>MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>Subsingleton α<VAR>f : α → β<GOAL>MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>TopologicalSpace β<GOAL>∀ {x : MeasurableSpace α} (hf : MeasureTheory.StronglyMeasurable f) (x_1 : α), Filter.Tendsto (fun n => ↑(hf.approx n) x_1) Filter.atTop (𝓝 (f x_1))
<VAR>α : Type u_1<VAR>β : Type u_5<VAR>f : α → β<VAR>NormedAddCommGroup β<VAR>NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>c : ℝ<VAR>x : α<VAR>hfx : ‖f x‖ ≤ c<GOAL>Filter.Tendsto (fun n => ↑(hf.approxBounded c n) x) Filter.atTop (𝓝 (f x))
<VAR>α : Type u_1<VAR>β : Type u_5<VAR>f : α → β<VAR>NormedAddCommGroup β<VAR>NormedSpace ℝ β<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>c : ℝ<VAR>hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => ↑(hf.approxBounded c n) x) Filter.atTop (𝓝 (f x))
<VAR>α : Type u_1<VAR>β : Type u_5<VAR>f : α → β<VAR>SeminormedAddCommGroup β<VAR>NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>c : ℝ<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>x : α<GOAL>‖↑(hf.approxBounded c n) x‖ ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>TopologicalSpace β<VAR>Nonempty β<VAR>T2Space β<GOAL>MeasureTheory.StronglyMeasurable f ↔ ∃ c, f = fun x => c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>TopologicalSpace β<VAR>Zero β<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hf_meas : MeasureTheory.StronglyMeasurable f<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hft_zero : ∀ x ∈ tᶜ, f x = 0<VAR>htμ : MeasureTheory.SigmaFinite (μ.restrict t)<GOAL>MeasureTheory.FinStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>TopologicalSpace β<VAR>Zero β<VAR>m0 : MeasurableSpace α<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>MeasureTheory.FinStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : MeasurableSpace β] [inst_3 : BorelSpace β], MeasureTheory.StronglyMeasurable f → Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : MeasurableSpace β] [inst_3 : BorelSpace β] {μ : MeasureTheory.Measure α}, MeasureTheory.StronglyMeasurable f → AEMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ] {g : β → γ} {f : α → β}, Continuous g → MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => g (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>m : MeasurableSpace α<VAR>Zero β<VAR>TopologicalSpace β<VAR>TopologicalSpace.MetrizableSpace β<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasurableSet (Function.support f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>m : MeasurableSpace α<VAR>One β<VAR>TopologicalSpace β<VAR>TopologicalSpace.MetrizableSpace β<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasurableSet (Function.mulSupport f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>m m' : MeasurableSpace α<VAR>TopologicalSpace β<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>h_mono : m' ≤ m<GOAL>MeasureTheory.StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α → β<VAR>g : α → γ<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>MeasureTheory.StronglyMeasurable fun x => (f x, g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace β<GOAL>∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace γ} {f : α → β} {g : γ → α}, MeasureTheory.StronglyMeasurable f → Measurable g → MeasureTheory.StronglyMeasurable (f ∘ g)