ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>Preorder α<VAR>OrderClosedTopology α<VAR>a : α<GOAL>MeasurableSet (Set.Ici a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>Preorder α<VAR>OrderClosedTopology α<VAR>a : α<GOAL>MeasurableSet (Set.Iic a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>Preorder α<VAR>OrderClosedTopology α<VAR>a b : α<GOAL>MeasurableSet (Set.Icc a b)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>PartialOrder α<VAR>OrderClosedTopology α<VAR>SecondCountableTopology α<GOAL>MeasurableSet {p | p.1 ≤ p.2}
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace δ<VAR>PartialOrder α<VAR>OrderClosedTopology α<VAR>SecondCountableTopology α<VAR>f g : δ → α<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>MeasurableSet {a | f a ≤ g a}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a : α<GOAL>MeasurableSet (Set.Iio a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a : α<GOAL>MeasurableSet (Set.Ioi a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a b : α<GOAL>MeasurableSet (Set.Ioo a b)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a b : α<GOAL>MeasurableSet (Set.Ioc a b)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a b : α<GOAL>MeasurableSet (Set.Ico a b)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>SecondCountableTopology α<GOAL>MeasurableSet {p | p.1 < p.2}
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>SecondCountableTopology α<VAR>f g : δ → α<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>MeasurableSet {a | f a < g a}
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>SecondCountableTopology α<VAR>μ : MeasureTheory.Measure δ<VAR>f g : δ → α<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>MeasureTheory.NullMeasurableSet {a | f a < g a} μ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>SecondCountableTopology α<VAR>μ : MeasureTheory.Measure (α × α)<GOAL>MeasureTheory.NullMeasurableSet {p | p.1 < p.2} μ
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>SecondCountableTopology α<VAR>μ : MeasureTheory.Measure δ<VAR>f g : δ → α<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>MeasureTheory.NullMeasurableSet {a | f a ≤ g a} μ
<VAR>α : Type u_1<VAR>s : Set α<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>h : s.OrdConnected<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>s : Set α<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>h : IsPreconnected s<GOAL>MeasurableSet s
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>s t : Set α<GOAL>MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Set.Ico l u = S} ≤ borel α
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>s : Set α<VAR>hd : Dense s<VAR>hbot : ∀ (x : α), IsBot x → x ∈ s<VAR>hIoo : ∀ (x y : α), x < y → Set.Ioo x y = ∅ → y ∈ s<GOAL>borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ico l u = S}
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>s : Set α<VAR>hd : Dense s<GOAL>borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ico l u = S}
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>OrderTopology α<GOAL>borel α = MeasurableSpace.generateFrom {S | ∃ l u, l < u ∧ Set.Ico l u = S}
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>s : Set α<VAR>hd : Dense s<VAR>hbot : ∀ (x : α), IsTop x → x ∈ s<VAR>hIoo : ∀ (x y : α), x < y → Set.Ioo x y = ∅ → x ∈ s<GOAL>borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ioc l u = S}
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>DenselyOrdered α<VAR>NoMaxOrder α<VAR>s : Set α<VAR>hd : Dense s<GOAL>borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ioc l u = S}
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>OrderTopology α<GOAL>borel α = MeasurableSpace.generateFrom {S | ∃ l u, l < u ∧ Set.Ioc l u = S}
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>BorelSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hμν : μ Set.univ = ν Set.univ<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Set.Ico a b) = ν (Set.Ico a b)<GOAL>μ = ν
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>BorelSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hμν : μ Set.univ = ν Set.univ<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Set.Ioc a b) = ν (Set.Ioc a b)<GOAL>μ = ν
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>BorelSpace α<VAR>NoMaxOrder α<VAR>μ ν : MeasureTheory.Measure α<VAR>hμ : ∀ ⦃a b : α⦄, a < b → μ (Set.Ico a b) ≠ ⊤<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Set.Ico a b) = ν (Set.Ico a b)<GOAL>μ = ν
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>BorelSpace α<VAR>NoMinOrder α<VAR>μ ν : MeasureTheory.Measure α<VAR>hμ : ∀ ⦃a b : α⦄, a < b → μ (Set.Ioc a b) ≠ ⊤<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Set.Ioc a b) = ν (Set.Ioc a b)<GOAL>μ = ν
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>_m : MeasurableSpace α<VAR>SecondCountableTopology α<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>BorelSpace α<VAR>NoMaxOrder α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Set.Ico a b) = ν (Set.Ico a b)<GOAL>μ = ν
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>_m : MeasurableSpace α<VAR>SecondCountableTopology α<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>BorelSpace α<VAR>NoMinOrder α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Set.Ioc a b) = ν (Set.Ioc a b)<GOAL>μ = ν
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>BorelSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h : ∀ (a : α), μ (Set.Iic a) = ν (Set.Iic a)<GOAL>μ = ν
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>BorelSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h : ∀ (a : α), μ (Set.Ici a) = ν (Set.Ici a)<GOAL>μ = ν
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a b : α<GOAL>MeasurableSet (Set.uIcc a b)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a b : α<GOAL>MeasurableSet (Ι a b)
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>SecondCountableTopology α<VAR>f g : δ → α<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun a => max (f a) (g a)
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>SecondCountableTopology α<VAR>f g : δ → α<VAR>μ : MeasureTheory.Measure δ<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun a => max (f a) (g a)) μ
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>SecondCountableTopology α<VAR>f g : δ → α<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun a => min (f a) (g a)
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>SecondCountableTopology α<VAR>f g : δ → α<VAR>μ : MeasureTheory.Measure δ<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun a => min (f a) (g a)) μ
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Iio x)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>TopologicalSpace δ<VAR>OpensMeasurableSpace δ<VAR>f : δ → α<VAR>hf : UpperSemicontinuous f<GOAL>Measurable f
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Ioi x)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>TopologicalSpace δ<VAR>OpensMeasurableSpace δ<VAR>f : δ → α<VAR>hf : LowerSemicontinuous f<GOAL>Measurable f
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Iic x)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Ici x)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Sort u_5<VAR>Countable ι<VAR>f : ι → δ → α<VAR>g : δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hg : ∀ (b : δ), IsLUB {a | ∃ i, f i b = a} (g b)<GOAL>Measurable g
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Sort u_5<VAR>Countable ι<VAR>f : ι → δ → α<VAR>g g' : δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>s : Set δ<VAR>hs : MeasurableSet s<VAR>hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)<VAR>hg' : Set.EqOn g g' sᶜ<VAR>g'_meas : Measurable g'<GOAL>Measurable g
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Sort u_5<VAR>μ : MeasureTheory.Measure δ<VAR>Countable ι<VAR>f : ι → δ → α<VAR>g : δ → α<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Sort u_5<VAR>Countable ι<VAR>f : ι → δ → α<VAR>g : δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hg : ∀ (b : δ), IsGLB {a | ∃ i, f i b = a} (g b)<GOAL>Measurable g
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Sort u_5<VAR>Countable ι<VAR>f : ι → δ → α<VAR>g g' : δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>s : Set δ<VAR>hs : MeasurableSet s<VAR>hg : ∀ b ∈ s, IsGLB {a | ∃ i, f i b = a} (g b)<VAR>hg' : Set.EqOn g g' sᶜ<VAR>g'_meas : Measurable g'<GOAL>Measurable g
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Sort u_5<VAR>μ : MeasureTheory.Measure δ<VAR>Countable ι<VAR>f : ι → δ → α<VAR>g : δ → α<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>TopologicalSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>LinearOrder β<VAR>OrderClosedTopology β<VAR>f : β → α<VAR>hf : Monotone f<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>TopologicalSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>LinearOrder β<VAR>OrderClosedTopology β<VAR>μ : MeasureTheory.Measure β<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>f : β → α<VAR>hf : MonotoneOn f s<GOAL>AEMeasurable f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>TopologicalSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>LinearOrder β<VAR>OrderClosedTopology β<VAR>f : β → α<VAR>hf : Antitone f<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>TopologicalSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>LinearOrder β<VAR>OrderClosedTopology β<VAR>μ : MeasureTheory.Measure β<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>f : β → α<VAR>hf : AntitoneOn f s<GOAL>AEMeasurable f (μ.restrict s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>s : Set α<VAR>h : ∀ x ∈ s, s ∈ 𝓝[>] x<VAR>h' : ∀ x ∈ s, ∃ y, x < y<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>s : Set α<VAR>h : ∀ x ∈ s, s ∈ 𝓝[>] x<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Sort u_5<VAR>Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<GOAL>MeasurableSet {b | BddAbove (Set.range fun i => f i b)}
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Sort u_5<VAR>Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<GOAL>MeasurableSet {b | BddBelow (Set.range fun i => f i b)}
<VAR>δ : Type u_4<VAR>MeasurableSpace δ<VAR>α : Type u_5<VAR>MeasurableSpace α<VAR>ConditionallyCompleteLattice α<VAR>p : Prop<VAR>f : δ → α<VAR>hf : Measurable f<GOAL>Measurable fun b => ⨆ (_ : p), f b
<VAR>δ : Type u_4<VAR>MeasurableSpace δ<VAR>α : Type u_5<VAR>MeasurableSpace α<VAR>ConditionallyCompleteLattice α<VAR>p : Prop<VAR>f : δ → α<VAR>hf : Measurable f<GOAL>Measurable fun b => ⨅ (_ : p), f b
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Sort u_5<VAR>Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<GOAL>Measurable fun b => ⨆ i, f i b
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Sort u_5<VAR>μ : MeasureTheory.Measure δ<VAR>Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<GOAL>AEMeasurable (fun b => ⨆ i, f i b) μ
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Sort u_5<VAR>Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<GOAL>Measurable fun b => ⨅ i, f i b
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Sort u_5<VAR>μ : MeasureTheory.Measure δ<VAR>Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<GOAL>AEMeasurable (fun b => ⨅ i, f i b) μ
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Type u_5<VAR>f : ι → δ → α<VAR>s : Set ι<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, Measurable (f i)<GOAL>Measurable fun x => sSup ((fun i => f i x) '' s)
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Type u_5<VAR>f : ι → δ → α<VAR>s : Set ι<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, Measurable (f i)<GOAL>Measurable fun x => sInf ((fun i => f i x) '' s)
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Type u_5<VAR>s : Set ι<VAR>f : ι → δ → α<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, Measurable (f i)<GOAL>Measurable fun b => ⨆ i ∈ s, f i b
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Type u_5<VAR>μ : MeasureTheory.Measure δ<VAR>s : Set ι<VAR>f : ι → δ → α<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<GOAL>AEMeasurable (fun b => ⨆ i ∈ s, f i b) μ
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Type u_5<VAR>s : Set ι<VAR>f : ι → δ → α<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, Measurable (f i)<GOAL>Measurable fun b => ⨅ i ∈ s, f i b
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Type u_5<VAR>μ : MeasureTheory.Measure δ<VAR>s : Set ι<VAR>f : ι → δ → α<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<GOAL>AEMeasurable (fun b => ⨅ i ∈ s, f i b) μ
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<GOAL>Measurable fun x => Filter.liminf (fun x_1 => f x_1 x) v
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>u : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hu : u.HasCountableBasis p s<VAR>hs : ∀ (i : ι'), (s i).Countable<GOAL>Measurable fun x => Filter.limsup (fun i => f i x) u
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>f : ℕ → δ → α<VAR>hf : ∀ (i : ℕ), Measurable (f i)<GOAL>Measurable fun x => Filter.liminf (fun i => f i x) Filter.atTop
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>MeasurableSpace δ<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>f : ℕ → δ → α<VAR>hf : ∀ (i : ℕ), Measurable (f i)<GOAL>Measurable fun x => Filter.limsup (fun i => f i x) Filter.atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>TopologicalSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>f : α ≃ₜ β<GOAL>MeasureTheory.IsFiniteMeasureOnCompacts (MeasureTheory.Measure.map (⇑f) μ)
<VAR>α : Type u_5<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<GOAL>μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' {⊤}) + ∑' (n : ℤ), μ (s ∩ f ⁻¹' Set.Ico (↑t ^ n) (↑t ^ (n + 1)))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>NormedLatticeAddCommGroup E<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>↑↑f ≤ᵐ[μ] ↑↑g ↔ f ≤ g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>NormedLatticeAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>0 ≤ᵐ[μ] ↑↑f ↔ 0 ≤ f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>NormedLatticeAddCommGroup E<VAR>f g : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hg : MeasureTheory.Memℒp g p μ<GOAL>MeasureTheory.Memℒp (f ⊔ g) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>NormedLatticeAddCommGroup E<VAR>f g : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hg : MeasureTheory.Memℒp g p μ<GOAL>MeasureTheory.Memℒp (f ⊓ g) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>NormedLatticeAddCommGroup E<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp |f| p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>NormedLatticeAddCommGroup E<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>↑↑(f ⊔ g) =ᵐ[μ] ↑↑f ⊔ ↑↑g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>NormedLatticeAddCommGroup E<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>↑↑(f ⊓ g) =ᵐ[μ] ↑↑f ⊓ ↑↑g