ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_5<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace β<VAR>MeasurableSpace β<VAR>OpensMeasurableSpace β<VAR>TopologicalSpace γ<VAR>MeasurableSpace γ<VAR>BorelSpace γ<VAR>MeasurableSpace δ<VAR>SecondCountableTopologyEither α β<VAR>f : δ → α<VAR>g : δ → β<VAR>c : α → β → γ<VAR>μ : MeasureTheory.Measure δ<VAR>h : Continuous fun p => c p.1 p.2<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun a => c (f a) (g a)) μ
<VAR>ι : Type u_6<VAR>π : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (π i)<VAR>(i : ι) → MeasurableSpace (π i)<VAR>∀ (i : ι), BorelSpace (π i)<GOAL>MeasurableSpace.pi ≤ borel ((i : ι) → π i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>TopologicalSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<GOAL>Prod.instMeasurableSpace ≤ borel (α × β)
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>hβ : BorelSpace β<VAR>e : α → β<VAR>h'e : MeasurableEmbedding e<VAR>h''e : Inducing e<GOAL>BorelSpace α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>TopologicalSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>f : α → β<VAR>h₁ : Embedding f<VAR>h₂ : MeasurableSet (Set.range f)<GOAL>MeasurableEmbedding f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>TopologicalSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>f : α → β<VAR>h : ClosedEmbedding f<GOAL>MeasurableEmbedding f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>TopologicalSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>f : α → β<VAR>h : OpenEmbedding f<GOAL>MeasurableEmbedding f
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>self : MeasureTheory.IsSetAlgebra 𝒜<GOAL>∅ ∈ 𝒜
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>self : MeasureTheory.IsSetAlgebra 𝒜<VAR>s : Set α<GOAL>s ∈ 𝒜 → sᶜ ∈ 𝒜
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>self : MeasureTheory.IsSetAlgebra 𝒜<VAR>s t : Set α<GOAL>s ∈ 𝒜 → t ∈ 𝒜 → s ∪ t ∈ 𝒜
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>h𝒜 : MeasureTheory.IsSetAlgebra 𝒜<GOAL>Set.univ ∈ 𝒜
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>s t : Set α<VAR>h𝒜 : MeasureTheory.IsSetAlgebra 𝒜<VAR>s_mem : s ∈ 𝒜<VAR>t_mem : t ∈ 𝒜<GOAL>s ∩ t ∈ 𝒜
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>s t : Set α<VAR>h𝒜 : MeasureTheory.IsSetAlgebra 𝒜<VAR>s_mem : s ∈ 𝒜<VAR>t_mem : t ∈ 𝒜<GOAL>s \ t ∈ 𝒜
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>h𝒜 : MeasureTheory.IsSetAlgebra 𝒜<GOAL>MeasureTheory.IsSetRing 𝒜
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>ι : Type u_2<VAR>h𝒜 : MeasureTheory.IsSetAlgebra 𝒜<VAR>s : ι → Set α<VAR>S : Finset ι<VAR>hs : ∀ i ∈ S, s i ∈ 𝒜<GOAL>⋃ i ∈ S, s i ∈ 𝒜
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>ι : Type u_2<VAR>h𝒜 : MeasureTheory.IsSetAlgebra 𝒜<VAR>s : ι → Set α<VAR>S : Finset ι<VAR>hs : ∀ i ∈ S, s i ∈ 𝒜<GOAL>⋂ i ∈ S, s i ∈ 𝒜
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<GOAL>MeasureTheory.IsSetAlgebra (MeasureTheory.generateSetAlgebra 𝒜)
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<GOAL>𝒜 ⊆ MeasureTheory.generateSetAlgebra 𝒜
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<GOAL>MeasurableSpace.generateFrom (MeasureTheory.generateSetAlgebra 𝒜) = MeasurableSpace.generateFrom 𝒜
<VAR>α : Type u_1<VAR>𝒜 ℬ : Set (Set α)<VAR>h : 𝒜 ⊆ ℬ<GOAL>MeasureTheory.generateSetAlgebra 𝒜 ⊆ MeasureTheory.generateSetAlgebra ℬ
<VAR>α : Type u_1<VAR>𝒜 ℬ : Set (Set α)<VAR>h : 𝒜 ⊆ ℬ<VAR>hℬ : MeasureTheory.IsSetAlgebra ℬ<GOAL>MeasureTheory.generateSetAlgebra 𝒜 ⊆ ℬ
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>h𝒜 : MeasureTheory.IsSetAlgebra 𝒜<GOAL>MeasureTheory.generateSetAlgebra 𝒜 ⊆ 𝒜
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>h𝒜 : MeasureTheory.IsSetAlgebra 𝒜<GOAL>MeasureTheory.generateSetAlgebra 𝒜 = 𝒜
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>s : Set α<VAR>s_mem : s ∈ MeasureTheory.generateSetAlgebra 𝒜<GOAL>∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ s = ⋃ a ∈ A, ⋂ t ∈ a, t
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>h : 𝒜.Countable<GOAL>(MeasureTheory.generateSetAlgebra 𝒜).Countable
<VAR>x y : ℝ<VAR>hxy : x < y<GOAL>Set.Icc x y ∈ (IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).setsAt x
<VAR>x : ℝ<GOAL>Filter.Tendsto (fun y => Set.Icc x y) (𝓝[>] x) ((IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).filterAt x)
<VAR>x y : ℝ<VAR>hxy : x < y<GOAL>Set.Icc x y ∈ (IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).setsAt y
<VAR>x : ℝ<GOAL>Filter.Tendsto (fun y => Set.Icc y x) (𝓝[<] x) ((IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).filterAt x)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : VitaliFamily μ<VAR>s : Set α<VAR>f : α → Set (Set α)<GOAL>(∀ x ∈ s, f x ⊆ self.setsAt x) → (∀ x ∈ s, ∀ ε > 0, ∃ a ∈ f x, a ⊆ Metric.closedBall x ε) → ∃ t, (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p => p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : VitaliFamily μ<VAR>x : α<VAR>s : Set α<GOAL>s ∈ self.setsAt x → (interior s).Nonempty
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : VitaliFamily μ<VAR>x : α<VAR>s : Set α<GOAL>s ∈ self.setsAt x → MeasurableSet s
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : VitaliFamily μ<VAR>x : α<VAR>ε : ℝ<GOAL>ε > 0 → ∃ s ∈ self.setsAt x, s ⊆ Metric.closedBall x ε
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : v.FineSubfamilyOn f s<GOAL>∃ t, (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p => p.2) ∧ (∀ p ∈ t, p.2 ∈ v.setsAt p.1 ∩ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : v.FineSubfamilyOn f s<VAR>p : α × Set α<GOAL>p ∈ h.index → p.1 ∈ s
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : v.FineSubfamilyOn f s<GOAL>h.index.PairwiseDisjoint h.covering
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : v.FineSubfamilyOn f s<GOAL>Pairwise (Disjoint on fun x => h.covering ↑x)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : v.FineSubfamilyOn f s<VAR>p : α × Set α<VAR>hp : p ∈ h.index<GOAL>h.covering p ∈ f p.1
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : v.FineSubfamilyOn f s<VAR>p : α × Set α<VAR>hp : p ∈ h.index<GOAL>h.covering p ∈ v.setsAt p.1
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : v.FineSubfamilyOn f s<GOAL>μ (s \ ⋃ p ∈ h.index, h.covering p) = 0
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : v.FineSubfamilyOn f s<VAR>SecondCountableTopology α<GOAL>h.index.Countable
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : v.FineSubfamilyOn f s<VAR>p : α × Set α<VAR>hp : p ∈ h.index<GOAL>MeasurableSet (h.covering p)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : v.FineSubfamilyOn f s<VAR>SecondCountableTopology α<VAR>ρ : MeasureTheory.Measure α<VAR>hρ : ρ ≪ μ<GOAL>ρ s ≤ ∑' (p : ↑h.index), ρ (h.covering ↑p)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : v.FineSubfamilyOn f s<VAR>SecondCountableTopology α<GOAL>μ s ≤ ∑' (x : ↑h.index), μ (h.covering ↑x)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>ι : Sort u_2<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>x : α<VAR>h : (𝓝 x).HasBasis p s<GOAL>(v.filterAt x).HasBasis p fun i => {t | t ∈ v.setsAt x ∧ t ⊆ s i}
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>x : α<GOAL>(v.filterAt x).HasBasis (fun x => 0 < x) fun x_1 => {a | a ∈ v.setsAt x ∧ a ⊆ Metric.closedBall x x_1}
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>x : α<VAR>s : Set (Set α)<GOAL>s ∈ v.filterAt x ↔ ∃ ε > 0, ∀ a ∈ v.setsAt x, a ⊆ Metric.closedBall x ε → a ∈ s
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>x : α<VAR>P : Set α → Prop<GOAL>(∀ᶠ (a : Set α) in v.filterAt x, P a) ↔ ∃ ε > 0, ∀ a ∈ v.setsAt x, a ⊆ Metric.closedBall x ε → P a
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>ι : Type u_2<VAR>l : Filter ι<VAR>f : ι → Set α<VAR>x : α<GOAL>Filter.Tendsto f l (v.filterAt x) ↔ (∀ᶠ (i : ι) in l, f i ∈ v.setsAt x) ∧ ∀ ε > 0, ∀ᶠ (i : ι) in l, f i ⊆ Metric.closedBall x ε
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>x : α<GOAL>∀ᶠ (a : Set α) in v.filterAt x, a ∈ v.setsAt x
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>x : α<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∀ᶠ (a : Set α) in v.filterAt x, a ⊆ Metric.closedBall x ε
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>x : α<GOAL>∀ᶠ (a : Set α) in v.filterAt x, MeasurableSet a
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>x : α<VAR>P : Set α → Prop<GOAL>(∃ᶠ (a : Set α) in v.filterAt x, P a) ↔ ∀ ε > 0, ∃ a ∈ v.setsAt x, a ⊆ Metric.closedBall x ε ∧ P a
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>x : α<VAR>o : Set α<VAR>hx : o ∈ 𝓝 x<GOAL>∀ᶠ (a : Set α) in v.filterAt x, a ⊆ o
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, a ∈ f x<GOAL>v.FineSubfamilyOn f s
<GOAL>borel ℝ = MeasurableSpace.generateFrom (⋃ a, ⋃ b, ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})
<GOAL>borel ℝ = MeasurableSpace.generateFrom (⋃ a, {Set.Iio ↑a})
<GOAL>borel ℝ = MeasurableSpace.generateFrom (⋃ a, {Set.Ioi ↑a})
<GOAL>borel ℝ = MeasurableSpace.generateFrom (⋃ a, {Set.Iic ↑a})
<GOAL>borel ℝ = MeasurableSpace.generateFrom (⋃ a, {Set.Ici ↑a})
<GOAL>IsPiSystem (⋃ a, ⋃ b, ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})
<GOAL>IsPiSystem (⋃ a, {Set.Iio ↑a})
<GOAL>IsPiSystem (⋃ a, {Set.Ioi ↑a})
<GOAL>IsPiSystem (⋃ a, {Set.Iic ↑a})
<GOAL>IsPiSystem (⋃ a, {Set.Ici ↑a})
<VAR>μ ν : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>h : ∀ (a b : ℚ), μ (Set.Ioo ↑a ↑b) = ν (Set.Ioo ↑a ↑b)<GOAL>μ = ν
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ<VAR>hf : Measurable f<GOAL>Measurable fun x => (f x).toNNReal
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => (f x).toNNReal) μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0<VAR>hf : Measurable f<GOAL>Measurable fun x => ↑(f x)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => ↑(f x)) μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ<VAR>hf : Measurable f<GOAL>Measurable fun x => ENNReal.ofReal (f x)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => ENNReal.ofReal (f x)) μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0<GOAL>(Measurable fun x => ↑(f x)) ↔ Measurable f
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0<VAR>μ : MeasureTheory.Measure α<GOAL>AEMeasurable (fun x => ↑(f x)) μ ↔ AEMeasurable f μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : ℝ≥0∞ → α<VAR>h : Measurable fun p => f ↑p<GOAL>Measurable f
<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>f : ℝ≥0∞ × β → γ<VAR>H₁ : Measurable fun p => f (↑p.1, p.2)<VAR>H₂ : Measurable fun x => f (⊤, x)<GOAL>Measurable f
<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>f : ℝ≥0∞ × ℝ≥0∞ → β<VAR>h₁ : Measurable fun p => f (↑p.1, ↑p.2)<VAR>h₂ : Measurable fun r => f (⊤, ↑r)<VAR>h₃ : Measurable fun r => f (↑r, ⊤)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>u : Filter ι<VAR>u.NeBot<VAR>u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>lim : Filter.Tendsto f u (𝓝 g)<GOAL>Measurable g
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>hf : ∀ (i : ℕ), Measurable (f i)<VAR>lim : Filter.Tendsto f Filter.atTop (𝓝 g)<GOAL>Measurable g
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>u : Filter ι<VAR>u.NeBot<VAR>u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hlim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) u (𝓝 (g a))<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>hf : ∀ (i : ℕ), AEMeasurable (f i) μ<VAR>hlim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (𝓝 (g a))<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable fun x => (f x).toNNReal
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => (f x).toNNReal) μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable fun x => (f x).toReal
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => (f x).toReal) μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>ι : Type u_5<VAR>Countable ι<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), Measurable (f i)<GOAL>Measurable fun x => ∑' (i : ι), f i x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>ι : Type u_5<VAR>Countable ι<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), Measurable (f i)<GOAL>Measurable (∑' (i : ι), f i)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>ι : Type u_5<VAR>Countable ι<VAR>f : ι → α → ℝ≥0<VAR>h : ∀ (i : ι), Measurable (f i)<GOAL>Measurable fun x => ∑' (i : ι), f i x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>ι : Type u_5<VAR>Countable ι<VAR>f : ι → α → ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>h : ∀ (i : ι), AEMeasurable (f i) μ<GOAL>AEMeasurable (fun x => ∑' (i : ι), f i x) μ
<VAR>α : Type u_5<VAR>MeasurableSpace α<VAR>ι : Type u_6<VAR>Countable ι<VAR>f : ι → α → ℝ≥0<VAR>μ : MeasureTheory.Measure α<VAR>h : ∀ (i : ι), AEMeasurable (f i) μ<GOAL>AEMeasurable (fun x => ∑' (i : ι), f i x) μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ<VAR>hf : Measurable f<GOAL>Measurable fun x => ↑(f x)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => ↑(f x)) μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : EReal → α<VAR>h : Measurable fun p => f ↑p<GOAL>Measurable f
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → EReal<VAR>hf : Measurable f<GOAL>Measurable fun x => (f x).toReal
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → EReal<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => (f x).toReal) μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable fun x => ↑(f x)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => ↑(f x)) μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0<VAR>g : α → ℝ≥0<VAR>u : Filter ι<VAR>u.NeBot<VAR>u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>lim : Filter.Tendsto f u (𝓝 g)<GOAL>Measurable g
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0<VAR>g : α → ℝ≥0<VAR>hf : ∀ (i : ℕ), Measurable (f i)<VAR>lim : Filter.Tendsto f Filter.atTop (𝓝 g)<GOAL>Measurable g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ≥0<VAR>hf : Measurable f<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ μ (s n) < ⊤ ∧ ∀ x ∈ s n, f x ≤ ↑n) ∧ ⋃ i, s i = Set.univ
<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>b : ℝ<GOAL>Filter.Tendsto (fun δ => μ (Set.Icc (b - δ) (b + δ))) (𝓝[>] 0) (𝓝 (μ {b}))
<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>b : ℝ<GOAL>Filter.Tendsto (fun δ => μ (Set.Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 (μ {b}))
<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>MeasureTheory.NoAtoms μ<VAR>b : ℝ<GOAL>Filter.Tendsto (fun δ => μ (Set.Icc (b - δ) (b + δ))) (𝓝 0) (𝓝 0)
<VAR>ι : Type u_2<VAR>α : ι → Type u_1<VAR>C : (i : ι) → Set (Set (α i))<GOAL>MeasureTheory.squareCylinders C = ⋃ s, (fun t => (↑s).pi t) '' Set.univ.pi C
<VAR>ι : Type u_2<VAR>α : ι → Type u_1<VAR>C : (i : ι) → Set (Set (α i))<VAR>hC : ∀ (i : ι), IsPiSystem (C i)<VAR>hC_univ : ∀ (i : ι), Set.univ ∈ C i<GOAL>IsPiSystem (MeasureTheory.squareCylinders C)
<VAR>ι : Type u_2<VAR>α : ι → Type u_1<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>i : ι<GOAL>MeasurableSpace.comap (Function.eval i) (m i) ≤ MeasurableSpace.generateFrom ((fun t => {i}.pi t) '' Set.univ.pi fun i => {s | MeasurableSet s})
<VAR>ι : Type u_2<VAR>α : ι → Type u_1<VAR>(i : ι) → MeasurableSpace (α i)<GOAL>MeasurableSpace.generateFrom (MeasureTheory.squareCylinders fun i => {s | MeasurableSet s}) = MeasurableSpace.pi
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>f : (i : ι) → α i<GOAL>f ∈ MeasureTheory.cylinder s S ↔ (fun i => f ↑i) ∈ S
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<GOAL>MeasureTheory.cylinder s ∅ = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<GOAL>MeasureTheory.cylinder s Set.univ = Set.univ
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>h_nonempty : Nonempty ((i : ι) → α i)<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<GOAL>MeasureTheory.cylinder s S = ∅ ↔ S = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s₁ s₂ : Finset ι<VAR>S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)<VAR>S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)<VAR>DecidableEq ι<GOAL>MeasureTheory.cylinder s₁ S₁ ∩ MeasureTheory.cylinder s₂ S₂ = MeasureTheory.cylinder (s₁ ∪ s₂) ((fun f j => f ⟨↑j, ⋯⟩) ⁻¹' S₁ ∩ (fun f j => f ⟨↑j, ⋯⟩) ⁻¹' S₂)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<VAR>S₁ S₂ : Set ((i : { x // x ∈ s }) → α ↑i)<GOAL>MeasureTheory.cylinder s S₁ ∩ MeasureTheory.cylinder s S₂ = MeasureTheory.cylinder s (S₁ ∩ S₂)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s₁ s₂ : Finset ι<VAR>S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)<VAR>S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)<VAR>DecidableEq ι<GOAL>MeasureTheory.cylinder s₁ S₁ ∪ MeasureTheory.cylinder s₂ S₂ = MeasureTheory.cylinder (s₁ ∪ s₂) ((fun f j => f ⟨↑j, ⋯⟩) ⁻¹' S₁ ∪ (fun f j => f ⟨↑j, ⋯⟩) ⁻¹' S₂)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<VAR>S₁ S₂ : Set ((i : { x // x ∈ s }) → α ↑i)<GOAL>MeasureTheory.cylinder s S₁ ∪ MeasureTheory.cylinder s S₂ = MeasureTheory.cylinder s (S₁ ∪ S₂)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<GOAL>(MeasureTheory.cylinder s S)ᶜ = MeasureTheory.cylinder s Sᶜ
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<VAR>S T : Set ((i : { x // x ∈ s }) → α ↑i)<GOAL>MeasureTheory.cylinder s S \ MeasureTheory.cylinder s T = MeasureTheory.cylinder s (S \ T)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>h_nonempty : Nonempty ((i : ι) → α i)<VAR>I J : Finset ι<VAR>S : Set ((i : { x // x ∈ I }) → α ↑i)<VAR>T : Set ((i : { x // x ∈ J }) → α ↑i)<VAR>h_eq : MeasureTheory.cylinder I S = MeasureTheory.cylinder J T<VAR>hJI : J ⊆ I<GOAL>S = (fun f j => f ⟨↑j, ⋯⟩) ⁻¹' T
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>I : Finset ι<VAR>S : Set ((i : { x // x ∈ I }) → α ↑i)<VAR>J : Finset ι<GOAL>MeasureTheory.cylinder I S = MeasureTheory.cylinder (I ∪ J) ((fun f j => f ⟨↑j, ⋯⟩) ⁻¹' S)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Nonempty ((i : ι) → α i)<VAR>s t : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>T : Set ((i : { x // x ∈ t }) → α ↑i)<VAR>DecidableEq ι<GOAL>Disjoint (MeasureTheory.cylinder s S) (MeasureTheory.cylinder t T) ↔ Disjoint ((fun f j => f ⟨↑j, ⋯⟩) ⁻¹' S) ((fun f j => f ⟨↑j, ⋯⟩) ⁻¹' T)
<VAR>ι : Type u_2<VAR>α : ι → Type u_1<VAR>(i : ι) → TopologicalSpace (α i)<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>hs : IsClosed S<GOAL>IsClosed (MeasureTheory.cylinder s S)
<VAR>ι : Type u_2<VAR>α : ι → Type u_1<VAR>(i : ι) → MeasurableSpace (α i)<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>hS : MeasurableSet S<GOAL>MeasurableSet (MeasureTheory.cylinder s S)
<VAR>ι : Type u_2<VAR>α : ι → Type u_1<VAR>(i : ι) → MeasurableSpace (α i)<GOAL>∅ ∈ MeasureTheory.measurableCylinders α
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>t : Set ((i : ι) → α i)<GOAL>t ∈ MeasureTheory.measurableCylinders α ↔ ∃ s S, MeasurableSet S ∧ t = MeasureTheory.cylinder s S
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>t : Set ((i : ι) → α i)<VAR>ht : t ∈ MeasureTheory.measurableCylinders α<GOAL>MeasurableSet (MeasureTheory.measurableCylinders.set ht)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>t : Set ((i : ι) → α i)<VAR>ht : t ∈ MeasureTheory.measurableCylinders α<GOAL>t = MeasureTheory.cylinder (MeasureTheory.measurableCylinders.finset ht) (MeasureTheory.measurableCylinders.set ht)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>hS : MeasurableSet S<GOAL>MeasureTheory.cylinder s S ∈ MeasureTheory.measurableCylinders α
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>s t : Set ((i : ι) → α i)<VAR>hs : s ∈ MeasureTheory.measurableCylinders α<VAR>ht : t ∈ MeasureTheory.measurableCylinders α<GOAL>s ∩ t ∈ MeasureTheory.measurableCylinders α
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<GOAL>IsPiSystem (MeasureTheory.measurableCylinders α)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>s : Set ((i : ι) → α i)<VAR>hs : s ∈ MeasureTheory.measurableCylinders α<GOAL>sᶜ ∈ MeasureTheory.measurableCylinders α
<VAR>ι : Type u_2<VAR>α : ι → Type u_1<VAR>(i : ι) → MeasurableSpace (α i)<GOAL>Set.univ ∈ MeasureTheory.measurableCylinders α
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>s t : Set ((i : ι) → α i)<VAR>hs : s ∈ MeasureTheory.measurableCylinders α<VAR>ht : t ∈ MeasureTheory.measurableCylinders α<GOAL>s ∪ t ∈ MeasureTheory.measurableCylinders α
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>s t : Set ((i : ι) → α i)<VAR>hs : s ∈ MeasureTheory.measurableCylinders α<VAR>ht : t ∈ MeasureTheory.measurableCylinders α<GOAL>s \ t ∈ MeasureTheory.measurableCylinders α
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<GOAL>MeasurableSpace.generateFrom (MeasureTheory.measurableCylinders α) = MeasurableSpace.pi