ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>TopologicalSpace α<VAR>ContinuousConstVAdd G α<VAR>AddAction.IsMinimal G α<VAR>K U : Set α<VAR>hK : IsCompact K<VAR>hμK : μ K ≠ 0<VAR>hU : IsOpen U<VAR>hne : U.Nonempty<GOAL>0 < μ U
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>TopologicalSpace α<VAR>ContinuousConstSMul G α<VAR>MulAction.IsMinimal G α<VAR>K U : Set α<VAR>hK : IsCompact K<VAR>hμK : μ K ≠ 0<VAR>hU : IsOpen U<VAR>hne : U.Nonempty<GOAL>0 < μ U
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>TopologicalSpace α<VAR>ContinuousConstSMul G α<VAR>MulAction.IsMinimal G α<VAR>U : Set α<VAR>hU : IsOpen U<VAR>hne : U.Nonempty<VAR>hμU : μ U ≠ ⊤<GOAL>MeasureTheory.IsLocallyFiniteMeasure μ
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>TopologicalSpace α<VAR>ContinuousConstVAdd G α<VAR>AddAction.IsMinimal G α<VAR>U : Set α<VAR>hU : IsOpen U<VAR>hne : U.Nonempty<VAR>hμU : μ U ≠ ⊤<GOAL>MeasureTheory.IsLocallyFiniteMeasure μ
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>TopologicalSpace α<VAR>ContinuousConstVAdd G α<VAR>AddAction.IsMinimal G α<VAR>U : Set α<VAR>μ.Regular<VAR>hμ : μ ≠ 0<VAR>hU : IsOpen U<VAR>hne : U.Nonempty<GOAL>0 < μ U
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>TopologicalSpace α<VAR>ContinuousConstSMul G α<VAR>MulAction.IsMinimal G α<VAR>U : Set α<VAR>μ.Regular<VAR>hμ : μ ≠ 0<VAR>hU : IsOpen U<VAR>hne : U.Nonempty<GOAL>0 < μ U
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>TopologicalSpace α<VAR>ContinuousConstSMul G α<VAR>MulAction.IsMinimal G α<VAR>U : Set α<VAR>μ.Regular<VAR>hμ : μ ≠ 0<VAR>hU : IsOpen U<GOAL>0 < μ U ↔ U.Nonempty
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>TopologicalSpace α<VAR>ContinuousConstVAdd G α<VAR>AddAction.IsMinimal G α<VAR>U : Set α<VAR>μ.Regular<VAR>hμ : μ ≠ 0<VAR>hU : IsOpen U<GOAL>0 < μ U ↔ U.Nonempty
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>TopologicalSpace α<VAR>ContinuousConstVAdd G α<VAR>AddAction.IsMinimal G α<VAR>U : Set α<VAR>μ.Regular<VAR>hμ : μ ≠ 0<VAR>hU : IsOpen U<GOAL>μ U = 0 ↔ U = ∅
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>TopologicalSpace α<VAR>ContinuousConstSMul G α<VAR>MulAction.IsMinimal G α<VAR>U : Set α<VAR>μ.Regular<VAR>hμ : μ ≠ 0<VAR>hU : IsOpen U<GOAL>μ U = 0 ↔ U = ∅
<VAR>self : StieltjesFunction<GOAL>Monotone ↑self
<VAR>self : StieltjesFunction<VAR>x : ℝ<GOAL>ContinuousWithinAt (↑self) (Set.Ici x) x
<VAR>f : StieltjesFunction<GOAL>Monotone ↑f
<VAR>f : StieltjesFunction<VAR>x : ℝ<GOAL>ContinuousWithinAt (↑f) (Set.Ici x) x
<VAR>f : StieltjesFunction<VAR>x : ℝ<GOAL>Function.rightLim (↑f) x = ↑f x
<VAR>f : StieltjesFunction<VAR>x : ℝ<GOAL>⨅ r, ↑f ↑r = ↑f x
<VAR>f : StieltjesFunction<VAR>x : ℝ<GOAL>⨅ r, ↑f ↑↑r = ↑f x
<VAR>a : ℝ<GOAL>↑StieltjesFunction.id a = id a
<VAR>x : ℝ<GOAL>Function.leftLim (↑StieltjesFunction.id) x = x
<VAR>c x : ℝ<GOAL>↑(StieltjesFunction.const c) x = c
<VAR>f g : StieltjesFunction<VAR>x : ℝ<GOAL>↑(f + g) x = ↑f x + ↑g x
<VAR>f : ℝ → ℝ<VAR>hf : Monotone f<VAR>x : ℝ<GOAL>↑hf.stieltjesFunction x = Function.rightLim f x
<VAR>f : StieltjesFunction<GOAL>{x | Function.leftLim (↑f) x ≠ ↑f x}.Countable
<VAR>f : StieltjesFunction<GOAL>f.length ∅ = 0
<VAR>f : StieltjesFunction<VAR>a b : ℝ<GOAL>f.length (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)
<VAR>f : StieltjesFunction<VAR>s₁ s₂ : Set ℝ<VAR>h : s₁ ⊆ s₂<GOAL>f.length s₁ ≤ f.length s₂
<VAR>f : StieltjesFunction<VAR>s : Set ℝ<GOAL>f.outer s ≤ f.length s
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>c d : ℕ → ℝ<VAR>ss : Set.Icc a b ⊆ ⋃ i, Set.Ioo (c i) (d i)<GOAL>ENNReal.ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ENNReal.ofReal (↑f (d i) - ↑f (c i))
<VAR>f : StieltjesFunction<VAR>a b : ℝ<GOAL>f.outer (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)
<VAR>f : StieltjesFunction<VAR>c : ℝ<GOAL>MeasurableSet (Set.Ioi c)
<VAR>f : StieltjesFunction<GOAL>f.measure = { toOuterMeasure := f.outer, m_iUnion := ⋯, trim_le := ⋯ }
<VAR>f : StieltjesFunction<VAR>a b : ℝ<GOAL>f.measure (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)
<VAR>f : StieltjesFunction<VAR>a : ℝ<GOAL>f.measure {a} = ENNReal.ofReal (↑f a - Function.leftLim (↑f) a)
<VAR>f : StieltjesFunction<VAR>a b : ℝ<GOAL>f.measure (Set.Icc a b) = ENNReal.ofReal (↑f b - Function.leftLim (↑f) a)
<VAR>f : StieltjesFunction<VAR>a b : ℝ<GOAL>f.measure (Set.Ioo a b) = ENNReal.ofReal (Function.leftLim (↑f) b - ↑f a)
<VAR>f : StieltjesFunction<VAR>a b : ℝ<GOAL>f.measure (Set.Ico a b) = ENNReal.ofReal (Function.leftLim (↑f) b - Function.leftLim (↑f) a)
<VAR>f : StieltjesFunction<VAR>l : ℝ<VAR>hf : Filter.Tendsto (↑f) Filter.atBot (𝓝 l)<VAR>x : ℝ<GOAL>f.measure (Set.Iic x) = ENNReal.ofReal (↑f x - l)
<VAR>f : StieltjesFunction<VAR>l : ℝ<VAR>hf : Filter.Tendsto (↑f) Filter.atTop (𝓝 l)<VAR>x : ℝ<GOAL>f.measure (Set.Ici x) = ENNReal.ofReal (l - Function.leftLim (↑f) x)
<VAR>f : StieltjesFunction<VAR>l u : ℝ<VAR>hfl : Filter.Tendsto (↑f) Filter.atBot (𝓝 l)<VAR>hfu : Filter.Tendsto (↑f) Filter.atTop (𝓝 u)<GOAL>f.measure Set.univ = ENNReal.ofReal (u - l)
<VAR>f : StieltjesFunction<VAR>l u : ℝ<VAR>hfl : Filter.Tendsto (↑f) Filter.atBot (𝓝 l)<VAR>hfu : Filter.Tendsto (↑f) Filter.atTop (𝓝 u)<GOAL>MeasureTheory.IsFiniteMeasure f.measure
<VAR>f : StieltjesFunction<VAR>hf_bot : Filter.Tendsto (↑f) Filter.atBot (𝓝 0)<VAR>hf_top : Filter.Tendsto (↑f) Filter.atTop (𝓝 1)<GOAL>MeasureTheory.IsProbabilityMeasure f.measure
<VAR>f g : StieltjesFunction<VAR>l : ℝ<VAR>hfg : f.measure = g.measure<VAR>hfl : Filter.Tendsto (↑f) Filter.atBot (𝓝 l)<VAR>hgl : Filter.Tendsto (↑g) Filter.atBot (𝓝 l)<GOAL>f = g
<VAR>f g : StieltjesFunction<VAR>y : ℝ<VAR>hfg : f.measure = g.measure<VAR>hy : ↑f y = ↑g y<GOAL>f = g
<VAR>c : ℝ<GOAL>(StieltjesFunction.const c).measure = 0
<VAR>f g : StieltjesFunction<GOAL>(f + g).measure = f.measure + g.measure
<VAR>c : ℝ≥0<VAR>f : StieltjesFunction<GOAL>(c • f).measure = c • f.measure
<VAR>M : Type u_1<VAR>Monoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>μ : MeasureTheory.Measure M<VAR>MeasureTheory.SFinite μ<GOAL>(MeasureTheory.Measure.dirac 1).mconv μ = μ
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>μ : MeasureTheory.Measure M<VAR>MeasureTheory.SFinite μ<GOAL>(MeasureTheory.Measure.dirac 0).conv μ = μ
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>μ : MeasureTheory.Measure M<VAR>MeasureTheory.SFinite μ<GOAL>μ.conv (MeasureTheory.Measure.dirac 0) = μ
<VAR>M : Type u_1<VAR>Monoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>μ : MeasureTheory.Measure M<VAR>MeasureTheory.SFinite μ<GOAL>μ.mconv (MeasureTheory.Measure.dirac 1) = μ
<VAR>M : Type u_1<VAR>Monoid M<VAR>MeasurableSpace M<VAR>μ : MeasureTheory.Measure M<GOAL>MeasureTheory.Measure.mconv 0 μ = 0
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>MeasurableSpace M<VAR>μ : MeasureTheory.Measure M<GOAL>MeasureTheory.Measure.conv 0 μ = 0
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>MeasurableSpace M<VAR>μ : MeasureTheory.Measure M<GOAL>μ.conv 0 = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>MeasurableSpace M<VAR>μ : MeasureTheory.Measure M<GOAL>μ.mconv 0 = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>μ ν ρ : MeasureTheory.Measure M<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite ρ<GOAL>μ.mconv (ν + ρ) = μ.mconv ν + μ.mconv ρ
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>μ ν ρ : MeasureTheory.Measure M<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite ρ<GOAL>μ.conv (ν + ρ) = μ.conv ν + μ.conv ρ
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>μ ν ρ : MeasureTheory.Measure M<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite ρ<GOAL>(μ + ν).conv ρ = μ.conv ρ + ν.conv ρ
<VAR>M : Type u_1<VAR>Monoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>μ ν ρ : MeasureTheory.Measure M<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite ρ<GOAL>(μ + ν).mconv ρ = μ.mconv ρ + ν.mconv ρ
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>μ ν : MeasureTheory.Measure M<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite ν<GOAL>μ.mconv ν = ν.mconv μ
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>μ ν : MeasureTheory.Measure M<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite ν<GOAL>μ.conv ν = ν.conv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p q : Set α → Prop<VAR>U : Set α<VAR>H : μ.InnerRegularWRT p q<VAR>hU : q U<GOAL>μ U = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p q : Set α → Prop<VAR>U : Set α<VAR>ε : ℝ≥0∞<VAR>H : μ.InnerRegularWRT p q<VAR>h0 : p ∅<VAR>hU : q U<VAR>hμU : μ U ≠ ⊤<VAR>hε : ε ≠ 0<GOAL>∃ K ⊆ U, p K ∧ μ U < μ K + ε
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>pa qa : Set α → Prop<VAR>H : μ.InnerRegularWRT pa qa<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>pb qb : Set β → Prop<VAR>hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)<VAR>hAB' : ∀ (K : Set α), pa K → pb (f '' K)<VAR>hB₂ : ∀ (U : Set β), qb U → MeasurableSet U<GOAL>(MeasureTheory.Measure.map f μ).InnerRegularWRT pb qb
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>pa qa : Set α → Prop<VAR>H : μ.InnerRegularWRT pa qa<VAR>f : α ≃ᵐ β<VAR>pb qb : Set β → Prop<VAR>hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)<VAR>hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)<GOAL>(MeasureTheory.Measure.map (⇑f) μ).InnerRegularWRT pb qb
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p q : Set α → Prop<VAR>H : μ.InnerRegularWRT p q<VAR>c : ℝ≥0∞<GOAL>(c • μ).InnerRegularWRT p q
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p q q' : Set α → Prop<VAR>H : μ.InnerRegularWRT p q<VAR>H' : μ.InnerRegularWRT q q'<GOAL>μ.InnerRegularWRT p q'
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : Set α → Prop<GOAL>μ.InnerRegularWRT p p
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p q : Set α → Prop<VAR>h : ∀ (s : Set α), q s → p s<GOAL>μ.InnerRegularWRT p q
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p q p' q' : Set α → Prop<VAR>H : μ.InnerRegularWRT p q<VAR>h : ∀ (s : Set α), q' s → q s<VAR>h' : ∀ (s : Set α), p s → p' s<GOAL>μ.InnerRegularWRT p' q'
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : μ.OuterRegular<VAR>A : Set α<GOAL>MeasurableSet A → ∀ r > μ A, ∃ U ⊇ A, IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : μ.Regular<GOAL>μ.InnerRegularWRT IsCompact IsOpen
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : μ.WeaklyRegular<GOAL>μ.InnerRegularWRT IsClosed IsOpen
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : μ.InnerRegular<GOAL>μ.InnerRegularWRT IsCompact fun s => MeasurableSet s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : μ.InnerRegularCompactLTTop<GOAL>μ.InnerRegularWRT IsCompact fun s => MeasurableSet s ∧ μ s ≠ ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.OuterRegular<VAR>A : Set α<VAR>r : ℝ≥0∞<VAR>hr : μ A < r<GOAL>∃ U ⊇ A, IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>A : Set α<VAR>μ : MeasureTheory.Measure α<VAR>μ.OuterRegular<GOAL>μ A = ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen U), μ U
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.OuterRegular<VAR>A : Set α<VAR>hA : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ U ⊇ A, IsOpen U ∧ μ U < μ A + ε
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>A : Set α<VAR>μ : MeasureTheory.Measure α<VAR>μ.OuterRegular<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ U ⊇ A, IsOpen U ∧ μ U ≤ μ A + ε
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.OuterRegular<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>hA' : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ U ⊇ A, IsOpen U ∧ μ U < ⊤ ∧ μ (U \ A) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>BorelSpace β<VAR>f : α ≃ₜ β<VAR>μ : MeasureTheory.Measure α<VAR>μ.OuterRegular<GOAL>(MeasureTheory.Measure.map (⇑f) μ).OuterRegular
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.OuterRegular<VAR>x : ℝ≥0∞<VAR>hx : x ≠ ⊤<GOAL>(x • μ).OuterRegular
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular<VAR>h' : ∀ (n : ℕ), IsOpen (s n)<VAR>h'' : Set.univ ⊆ ⋃ n, s n<GOAL>μ.OuterRegular
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>R1Space α<VAR>μ.OuterRegular<VAR>k : Set α<VAR>hk : IsCompact k<GOAL>μ (closure k) = μ k
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : μ.FiniteSpanningSetsIn {U | IsOpen U ∧ (μ.restrict U).OuterRegular}<GOAL>μ.OuterRegular
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : Set α → Prop<VAR>μ.OuterRegular<VAR>H : μ.InnerRegularWRT p IsOpen<VAR>hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)<GOAL>μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>H : μ.InnerRegularWRT IsClosed IsOpen<GOAL>μ.WeaklyRegular
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : Set α → Prop<VAR>μ : MeasureTheory.Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet<VAR>hs : Set.univ ⊆ ⋃ n, s n<VAR>hmono : Monotone s<GOAL>μ.InnerRegularWRT p MeasurableSet
<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace.PseudoMetrizableSpace X<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<GOAL>μ.InnerRegularWRT IsClosed IsOpen
<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>SigmaCompactSpace X<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<GOAL>μ.InnerRegularWRT IsCompact IsClosed
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : Set α → Prop<VAR>h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤<VAR>A : Set α<GOAL>(μ.restrict A).InnerRegularWRT p fun s => MeasurableSet s ∧ (μ.restrict A) s ≠ ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : Set α → Prop<VAR>h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤<VAR>A : Set α<VAR>hA : μ A ≠ ⊤<GOAL>(μ.restrict A).InnerRegularWRT p fun s => MeasurableSet s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>μ.InnerRegularWRT (fun s => MeasurableSet s ∧ μ s ≠ ⊤) fun s => MeasurableSet s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>U : Set α<VAR>hU : MeasurableSet U<VAR>μ : MeasureTheory.Measure α<VAR>μ.InnerRegular<GOAL>μ U = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), μ K
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>R1Space α<VAR>OpensMeasurableSpace α<VAR>h : μ.InnerRegular<GOAL>μ.InnerRegularWRT IsClosed IsOpen
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.InnerRegular<GOAL>(∃ K, IsCompact K ∧ μ K ≠ 0) ↔ μ ≠ 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.InnerRegular<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>r : ℝ≥0∞<VAR>hr : r < μ A<GOAL>∃ K ⊆ A, IsCompact K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>BorelSpace α<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>BorelSpace β<VAR>h : μ.InnerRegular<VAR>f : α → β<VAR>hf : Continuous f<GOAL>(MeasureTheory.Measure.map f μ).InnerRegular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>BorelSpace α<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>BorelSpace β<VAR>μ.InnerRegular<VAR>f : α ≃ₜ β<GOAL>(MeasureTheory.Measure.map (⇑f) μ).InnerRegular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>BorelSpace α<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>BorelSpace β<VAR>f : α ≃ₜ β<GOAL>(MeasureTheory.Measure.map (⇑f) μ).InnerRegular ↔ μ.InnerRegular
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.InnerRegularCompactLTTop<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ K ⊆ A, IsCompact K ∧ μ A < μ K + ε
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.InnerRegularCompactLTTop<VAR>R1Space α<VAR>BorelSpace α<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ K ⊆ A, IsCompact K ∧ IsClosed K ∧ μ A < μ K + ε
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>OpensMeasurableSpace α<VAR>T2Space α<VAR>μ.InnerRegularCompactLTTop<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ K ⊆ A, IsCompact K ∧ μ (A \ K) < ε
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>BorelSpace α<VAR>R1Space α<VAR>μ.InnerRegularCompactLTTop<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ K ⊆ A, IsCompact K ∧ IsClosed K ∧ μ (A \ K) < ε
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.InnerRegularCompactLTTop<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<VAR>r : ℝ≥0∞<VAR>hr : r < μ A<GOAL>∃ K ⊆ A, IsCompact K ∧ r < μ K
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.InnerRegularCompactLTTop<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<GOAL>μ A = ⨆ K, ⨆ (_ : K ⊆ A), ⨆ (_ : IsCompact K), μ K
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.InnerRegularCompactLTTop<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>R1Space α<VAR>BorelSpace α<VAR>K : Set α<VAR>hK : IsCompact K<VAR>r : ℝ≥0∞<VAR>hr : μ K < r<GOAL>∃ U, K ⊆ U ∧ IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.InnerRegularCompactLTTop<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>R1Space α<VAR>BorelSpace α<VAR>K : Set α<VAR>hK : IsCompact K<GOAL>μ K = ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen U), μ U
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.InnerRegularCompactLTTop<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>R1Space α<VAR>BorelSpace α<VAR>K : Set α<VAR>hK : IsCompact K<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ U, K ⊆ U ∧ IsOpen U ∧ μ U < μ K + ε
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.InnerRegularCompactLTTop<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>R1Space α<VAR>BorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (U ∆ s) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>BorelSpace α<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>BorelSpace β<VAR>h : μ.InnerRegularCompactLTTop<VAR>f : α → β<VAR>hf : Continuous f<GOAL>(MeasureTheory.Measure.map f μ).InnerRegularCompactLTTop
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<VAR>U : Set α<VAR>hU : IsOpen U<VAR>r : ℝ≥0∞<VAR>hr : r < μ U<GOAL>∃ F ⊆ U, IsClosed F ∧ r < μ F
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>U : Set α<VAR>hU : IsOpen U<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<GOAL>μ U = ⨆ F, ⨆ (_ : F ⊆ U), ⨆ (_ : IsClosed F), μ F
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<GOAL>μ.InnerRegularWRT IsClosed fun s => MeasurableSet s ∧ μ s ≠ ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ K ⊆ s, IsClosed K ∧ μ s < μ K + ε
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>OpensMeasurableSpace α<VAR>μ.WeaklyRegular<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ F ⊆ A, IsClosed F ∧ μ (A \ F) < ε
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<VAR>r : ℝ≥0∞<VAR>hr : r < μ A<GOAL>∃ K ⊆ A, IsClosed K ∧ r < μ K
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<GOAL>μ A = ⨆ K, ⨆ (_ : K ⊆ A), ⨆ (_ : IsClosed K), μ K
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>BorelSpace α<VAR>μ.WeaklyRegular<VAR>A : Set α<VAR>h'A : μ A ≠ ⊤<GOAL>(μ.restrict A).WeaklyRegular
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<VAR>x : ℝ≥0∞<VAR>hx : x ≠ ⊤<GOAL>(x • μ).WeaklyRegular
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.Regular<VAR>U : Set α<VAR>hU : IsOpen U<VAR>r : ℝ≥0∞<VAR>hr : r < μ U<GOAL>∃ K ⊆ U, IsCompact K ∧ r < μ K
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>U : Set α<VAR>hU : IsOpen U<VAR>μ : MeasureTheory.Measure α<VAR>μ.Regular<GOAL>μ U = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), μ K
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.Regular<GOAL>(∃ K, IsCompact K ∧ μ K ≠ 0) ↔ μ ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>BorelSpace α<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>BorelSpace β<VAR>μ.Regular<VAR>f : α ≃ₜ β<GOAL>(MeasureTheory.Measure.map (⇑f) μ).Regular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>μ : MeasureTheory.Measure α<VAR>BorelSpace α<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>BorelSpace β<VAR>f : α ≃ₜ β<GOAL>(MeasureTheory.Measure.map (⇑f) μ).Regular ↔ μ.Regular