ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f g : α → ℝ<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.Integrable g μ<VAR>c : ℝ<VAR>hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c<GOAL>μ[f * g|m] =ᵐ[μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f g : α → ℝ<VAR>hf : MeasureTheory.AEStronglyMeasurable' m f μ<VAR>hg : MeasureTheory.Integrable g μ<VAR>c : ℝ<VAR>hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c<GOAL>μ[f * g|m] =ᵐ[μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hfg : MeasureTheory.Integrable (f * g) μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>μ[f * g|m] =ᵐ[μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>hf : MeasureTheory.AEStronglyMeasurable' m f μ<VAR>hfg : MeasureTheory.Integrable (f * g) μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>μ[f * g|m] =ᵐ[μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s : Set α<GOAL>(MeasureTheory.OuterMeasure.ofFunction m m_empty) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), m (t n)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s : Set α<GOAL>(MeasureTheory.OuterMeasure.ofFunction m m_empty) s ≤ m s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s : Set α<VAR>m_mono : ∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t<VAR>m_subadd : ∀ (s : ℕ → Set α), m (⋃ i, s i) ≤ ∑' (i : ℕ), m (s i)<GOAL>(MeasureTheory.OuterMeasure.ofFunction m m_empty) s = m s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>μ : MeasureTheory.OuterMeasure α<GOAL>μ ≤ MeasureTheory.OuterMeasure.ofFunction m m_empty ↔ ∀ (s : Set α), μ s ≤ m s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<GOAL>IsGreatest {μ | ∀ (s : Set α), μ s ≤ m s} (MeasureTheory.OuterMeasure.ofFunction m m_empty)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<GOAL>MeasureTheory.OuterMeasure.ofFunction m m_empty = sSup {μ | ∀ (s : Set α), μ s ≤ m s}
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s t : Set α<VAR>h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤<GOAL>(MeasureTheory.OuterMeasure.ofFunction m m_empty) (s ∪ t) = (MeasureTheory.OuterMeasure.ofFunction m m_empty) s + (MeasureTheory.OuterMeasure.ofFunction m m_empty) t
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>β : Type u_2<VAR>f : β → α<VAR>h : Monotone m ∨ Function.Surjective f<GOAL>(MeasureTheory.OuterMeasure.comap f) (MeasureTheory.OuterMeasure.ofFunction m m_empty) = MeasureTheory.OuterMeasure.ofFunction (fun s => m (f '' s)) ⋯
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>β : Type u_2<VAR>f : α → β<GOAL>(MeasureTheory.OuterMeasure.map f) (MeasureTheory.OuterMeasure.ofFunction m m_empty) ≤ MeasureTheory.OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>(MeasureTheory.OuterMeasure.map f) (MeasureTheory.OuterMeasure.ofFunction m m_empty) = MeasureTheory.OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s : Set α<VAR>hm : Monotone m<GOAL>(MeasureTheory.OuterMeasure.restrict s) (MeasureTheory.OuterMeasure.ofFunction m m_empty) = MeasureTheory.OuterMeasure.ofFunction (fun t => m (t ∩ s)) ⋯
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>c • MeasureTheory.OuterMeasure.ofFunction m m_empty = MeasureTheory.OuterMeasure.ofFunction (c • m) ⋯
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<GOAL>(MeasureTheory.OuterMeasure.boundedBy m) s ≤ m s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s : Set α<GOAL>(MeasureTheory.OuterMeasure.boundedBy m) s = (MeasureTheory.OuterMeasure.ofFunction m m_empty) s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<GOAL>(MeasureTheory.OuterMeasure.boundedBy m) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (t n)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<VAR>m_empty : m ∅ = 0<VAR>m_mono : ∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t<VAR>m_subadd : ∀ (s : ℕ → Set α), m (⋃ i, s i) ≤ ∑' (i : ℕ), m (s i)<GOAL>(MeasureTheory.OuterMeasure.boundedBy m) s = m s
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<GOAL>MeasureTheory.OuterMeasure.boundedBy ⇑m = m
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>μ : MeasureTheory.OuterMeasure α<GOAL>μ ≤ MeasureTheory.OuterMeasure.boundedBy m ↔ ∀ (s : Set α), μ s ≤ m s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>μ : MeasureTheory.OuterMeasure α<GOAL>μ ≤ MeasureTheory.OuterMeasure.boundedBy m ↔ ∀ (s : Set α), s.Nonempty → μ s ≤ m s
<VAR>α : Type u_1<GOAL>MeasureTheory.OuterMeasure.boundedBy ⊤ = ⊤
<VAR>α : Type u_1<GOAL>MeasureTheory.OuterMeasure.boundedBy 0 = 0
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>c • MeasureTheory.OuterMeasure.boundedBy m = MeasureTheory.OuterMeasure.boundedBy (c • m)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>β : Type u_2<VAR>f : β → α<VAR>h : (Monotone fun s => m ↑s) ∨ Function.Surjective f<GOAL>(MeasureTheory.OuterMeasure.comap f) (MeasureTheory.OuterMeasure.boundedBy m) = MeasureTheory.OuterMeasure.boundedBy fun s => m (f '' s)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s t : Set α<VAR>h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤<GOAL>(MeasureTheory.OuterMeasure.boundedBy m) (s ∪ t) = (MeasureTheory.OuterMeasure.boundedBy m) s + (MeasureTheory.OuterMeasure.boundedBy m) t
<VAR>α : Type u_1<VAR>m : Set (MeasureTheory.OuterMeasure α)<VAR>t : Set α<GOAL>MeasureTheory.OuterMeasure.sInfGen m t = ⨅ μ ∈ m, μ t
<VAR>α : Type u_1<VAR>m : Set (MeasureTheory.OuterMeasure α)<GOAL>sInf m = MeasureTheory.OuterMeasure.boundedBy (MeasureTheory.OuterMeasure.sInfGen m)
<VAR>α : Type u_1<VAR>m : Set (MeasureTheory.OuterMeasure α)<VAR>h : m.Nonempty<VAR>t : Set α<GOAL>⨆ (_ : t.Nonempty), MeasureTheory.OuterMeasure.sInfGen m t = ⨅ μ ∈ m, μ t
<VAR>α : Type u_1<VAR>m : Set (MeasureTheory.OuterMeasure α)<VAR>s : Set α<VAR>h : m.Nonempty<GOAL>(sInf m) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, μ (t n)
<VAR>α : Type u_1<VAR>m : Set (MeasureTheory.OuterMeasure α)<VAR>s : Set α<VAR>h : s.Nonempty<GOAL>(sInf m) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, μ (t n)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>Nonempty ι<VAR>m : ι → MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>(⨅ i, m i) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>m : ι → MeasureTheory.OuterMeasure α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>(⨅ i, m i) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>I : Set ι<VAR>hI : I.Nonempty<VAR>m : ι → MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>(⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i) (t n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>I : Set ι<VAR>m : ι → MeasureTheory.OuterMeasure α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>(⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i) (t n)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>m : ι → MeasureTheory.OuterMeasure α<GOAL>(MeasureTheory.OuterMeasure.map f) (⨅ i, m i) ≤ ⨅ i, (MeasureTheory.OuterMeasure.map f) (m i)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>m : ι → MeasureTheory.OuterMeasure β<GOAL>(MeasureTheory.OuterMeasure.comap f) (⨅ i, m i) = ⨅ i, (MeasureTheory.OuterMeasure.comap f) (m i)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>m : ι → MeasureTheory.OuterMeasure α<GOAL>(MeasureTheory.OuterMeasure.map f) (⨅ i, m i) = (MeasureTheory.OuterMeasure.restrict (Set.range f)) (⨅ i, (MeasureTheory.OuterMeasure.map f) (m i))
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>Nonempty ι<VAR>f : α → β<VAR>m : ι → MeasureTheory.OuterMeasure β<GOAL>(MeasureTheory.OuterMeasure.map f) (⨅ i, (MeasureTheory.OuterMeasure.comap f) (m i)) = ⨅ i, (MeasureTheory.OuterMeasure.map f) ((MeasureTheory.OuterMeasure.comap f) (m i))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>I : Set ι<VAR>hI : I.Nonempty<VAR>f : α → β<VAR>m : ι → MeasureTheory.OuterMeasure β<GOAL>(MeasureTheory.OuterMeasure.map f) (⨅ i ∈ I, (MeasureTheory.OuterMeasure.comap f) (m i)) = ⨅ i ∈ I, (MeasureTheory.OuterMeasure.map f) ((MeasureTheory.OuterMeasure.comap f) (m i))
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>s : Set α<VAR>m : ι → MeasureTheory.OuterMeasure α<GOAL>(MeasureTheory.OuterMeasure.restrict s) (⨅ i, (MeasureTheory.OuterMeasure.restrict s) (m i)) = (MeasureTheory.OuterMeasure.restrict s) (⨅ i, m i)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>Nonempty ι<VAR>s : Set α<VAR>m : ι → MeasureTheory.OuterMeasure α<GOAL>(MeasureTheory.OuterMeasure.restrict s) (⨅ i, m i) = ⨅ i, (MeasureTheory.OuterMeasure.restrict s) (m i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>I : Set ι<VAR>hI : I.Nonempty<VAR>s : Set α<VAR>m : ι → MeasureTheory.OuterMeasure α<GOAL>(MeasureTheory.OuterMeasure.restrict s) (⨅ i ∈ I, m i) = ⨅ i ∈ I, (MeasureTheory.OuterMeasure.restrict s) (m i)
<VAR>α : Type u_1<VAR>m : Set (MeasureTheory.OuterMeasure α)<VAR>s : Set α<VAR>hm : m.Nonempty<GOAL>(MeasureTheory.OuterMeasure.restrict s) (sInf m) = sInf (⇑(MeasureTheory.OuterMeasure.restrict s) '' m)
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>m : (s : α) → P s → ℝ≥0∞<VAR>s : α<VAR>h : P s<GOAL>MeasureTheory.extend m s = m s h
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>m : (s : α) → P s → ℝ≥0∞<VAR>s : α<VAR>h : ¬P s<GOAL>MeasureTheory.extend m s = ⊤
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>m : (s : α) → P s → ℝ≥0∞<VAR>R : Type u_2<VAR>Zero R<VAR>SMulWithZero R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>NoZeroSMulDivisors R ℝ≥0∞<VAR>c : R<VAR>hc : c ≠ 0<GOAL>c • MeasureTheory.extend m = MeasureTheory.extend fun s h => c • m s h
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>m : (s : α) → P s → ℝ≥0∞<VAR>s : α<VAR>h : P s<GOAL>m s h ≤ MeasureTheory.extend m s
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>m : (s : α) → P s → ℝ≥0∞<VAR>β : Type u_2<VAR>Pb : β → Prop<VAR>mb : (s : β) → Pb s → ℝ≥0∞<VAR>sa : α<VAR>sb : β<VAR>hP : P sa ↔ Pb sb<VAR>hm : ∀ (ha : P sa) (hb : Pb sb), m sa ha = mb sb hb<GOAL>MeasureTheory.extend m sa = MeasureTheory.extend mb sb
<VAR>α : Type u_2<VAR>P : α → Prop<GOAL>(MeasureTheory.extend fun x x => ⊤) = ⊤
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<GOAL>MeasureTheory.extend m ∅ = 0
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>f : ℕ → Set α<VAR>hm : ∀ (i : ℕ), P (f i)<VAR>mU : m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<GOAL>MeasureTheory.extend m (⋃ i, f i) = ∑' (i : ℕ), MeasureTheory.extend m (f i)
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>s : ℕ → Set α<GOAL>MeasureTheory.extend m (⋃ i, s i) ≤ ∑' (i : ℕ), MeasureTheory.extend m (s i)
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s₁ s₂ : Set α<VAR>h₁ : P s₁<VAR>hs : s₁ ⊆ s₂<GOAL>MeasureTheory.extend m s₁ ≤ MeasureTheory.extend m s₂
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>β : Type u_2<VAR>Countable β<VAR>f : β → Set α<VAR>hd : Pairwise (Disjoint on f)<VAR>hm : ∀ (i : β), P (f i)<GOAL>MeasureTheory.extend m (⋃ i, f i) = ∑' (i : β), MeasureTheory.extend m (f i)
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>s₁ s₂ : Set α<VAR>hd : Disjoint s₁ s₂<VAR>h₁ : P s₁<VAR>h₂ : P s₂<GOAL>MeasureTheory.extend m (s₁ ∪ s₂) = MeasureTheory.extend m s₁ + MeasureTheory.extend m s₂
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>μ : MeasureTheory.OuterMeasure α<GOAL>μ ≤ MeasureTheory.inducedOuterMeasure m P0 m0 ↔ ∀ (s : Set α) (hs : P s), μ s ≤ m s hs
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>s t : Set α<VAR>h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → ¬P u<GOAL>(MeasureTheory.inducedOuterMeasure m P0 m0) (s ∪ t) = (MeasureTheory.inducedOuterMeasure m P0 m0) s + (MeasureTheory.inducedOuterMeasure m P0 m0) t
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s : Set α<VAR>hs : P s<GOAL>(MeasureTheory.inducedOuterMeasure m P0 m0) s = MeasureTheory.extend m s
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s : Set α<VAR>hs : P s<GOAL>(MeasureTheory.inducedOuterMeasure m P0 m0) s = m s hs
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s : Set α<GOAL>(MeasureTheory.inducedOuterMeasure m P0 m0) s = ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>f : α ≃ α<VAR>Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s<VAR>mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs<VAR>A : Set α<GOAL>(MeasureTheory.inducedOuterMeasure m P0 m0) (⇑f ⁻¹' A) = (MeasureTheory.inducedOuterMeasure m P0 m0) A
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s : Set α<VAR>hs : (MeasureTheory.inducedOuterMeasure m P0 m0) s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ t, P t ∧ s ⊆ t ∧ (MeasureTheory.inducedOuterMeasure m P0 m0) t ≤ (MeasureTheory.inducedOuterMeasure m P0 m0) s + ε
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s : Set α<GOAL>MeasurableSet s ↔ ∀ (t : Set α), P t → (MeasureTheory.inducedOuterMeasure m P0 m0) (t ∩ s) + (MeasureTheory.inducedOuterMeasure m P0 m0) (t \ s) ≤ (MeasureTheory.inducedOuterMeasure m P0 m0) t
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>hs : s₁ ⊆ s₂<GOAL>MeasureTheory.extend m s₁ ≤ MeasureTheory.extend m s₂
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>s : ℕ → Set α<GOAL>MeasureTheory.extend m (⋃ i, s i) ≤ ∑' (i : ℕ), MeasureTheory.extend m (s i)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.inducedOuterMeasure m ⋯ m0) s = MeasureTheory.extend m s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.inducedOuterMeasure m ⋯ m0) s = m s hs
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m₁ m₂ : MeasureTheory.OuterMeasure α<GOAL>m₁ ≤ m₂.trim ↔ ∀ (s : Set α), MeasurableSet s → m₁ s ≤ m₂ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m : MeasureTheory.OuterMeasure α<GOAL>m ≤ m.trim
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>m.trim s = m s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m₁ m₂ : MeasureTheory.OuterMeasure α<VAR>H : ∀ {s : Set α}, MeasurableSet s → m₁ s = m₂ s<GOAL>m₁.trim = m₂.trim
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>Monotone MeasureTheory.OuterMeasure.trim
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<VAR>m0 m1 : MeasurableSpace α<VAR>h : m0 ≤ m1<GOAL>m.trim ≤ m.trim
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m₁ m₂ : MeasureTheory.OuterMeasure α<GOAL>m₁.trim ≤ m₂.trim ↔ ∀ (s : Set α), MeasurableSet s → m₁ s ≤ m₂ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m₁ m₂ : MeasureTheory.OuterMeasure α<GOAL>m₁.trim = m₂.trim ↔ ∀ (s : Set α), MeasurableSet s → m₁ s = m₂ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>m.trim s = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>m.trim s = ⨅ t, m ↑t
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m : MeasureTheory.OuterMeasure α<GOAL>m.trim.trim = m.trim
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>⊤.trim = ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>MeasureTheory.OuterMeasure.trim 0 = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>ι : Type u_2<VAR>m : ι → MeasureTheory.OuterMeasure α<GOAL>(MeasureTheory.OuterMeasure.sum fun i => (m i).trim) ≤ (MeasureTheory.OuterMeasure.sum m).trim
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = m.trim s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set α<VAR>h : m.trim s = 0<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>ι : Sort u_2<VAR>Countable ι<VAR>μ : ι → MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m₁ m₂ m₃ : MeasureTheory.OuterMeasure α<VAR>op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞<VAR>h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)<VAR>s : Set α<GOAL>m₁.trim s = op (m₂.trim s) (m₃.trim s)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m₁ m₂ : MeasureTheory.OuterMeasure α<VAR>op : ℝ≥0∞ → ℝ≥0∞<VAR>h : ∀ (s : Set α), m₁ s = op (m₂ s)<VAR>s : Set α<GOAL>m₁.trim s = op (m₂.trim s)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m₁ m₂ : MeasureTheory.OuterMeasure α<GOAL>(m₁ + m₂).trim = m₁.trim + m₂.trim
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>R : Type u_2<VAR>SMul R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>c : R<VAR>m : MeasureTheory.OuterMeasure α<GOAL>(c • m).trim = c • m.trim
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m₁ m₂ : MeasureTheory.OuterMeasure α<GOAL>(m₁ ⊔ m₂).trim = m₁.trim ⊔ m₂.trim
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>ι : Sort u_2<VAR>Countable ι<VAR>μ : ι → MeasureTheory.OuterMeasure α<GOAL>(⨆ i, μ i).trim = ⨆ i, (μ i).trim
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.OuterMeasure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>((MeasureTheory.OuterMeasure.restrict s) μ).trim = (MeasureTheory.OuterMeasure.restrict s) μ.trim
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>self : MeasurableEmbedding f<VAR>s : Set α<GOAL>MeasurableSet s → MeasurableSet (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>self : MeasurableEmbedding f<GOAL>Function.Injective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>self : MeasurableEmbedding f<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<GOAL>MeasurableSet (f '' s) ↔ MeasurableSet s
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<GOAL>MeasurableEmbedding id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : MeasurableEmbedding g<VAR>hf : MeasurableEmbedding f<GOAL>MeasurableEmbedding (g ∘ f)
<VAR>α : Type u_1<VAR>s : Set α<VAR>mα : MeasurableSpace α<VAR>hs : MeasurableSet s<GOAL>MeasurableEmbedding Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<GOAL>MeasurableSet (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>s : Set β<GOAL>MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<GOAL>Measurable (Set.rangeSplitting f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>g : α → γ<VAR>g' : β → γ<VAR>hg : Measurable g<VAR>hg' : Measurable g'<GOAL>Measurable (Function.extend f g g')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>g : α → γ<VAR>hg : Measurable g<VAR>hne : β → Nonempty γ<GOAL>∃ g', Measurable g' ∧ g' ∘ f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : MeasurableEmbedding g<GOAL>Measurable (g ∘ f) ↔ Measurable f
<VAR>α : Type u_1<VAR>s : Set α<GOAL>∀ {x : MeasurableSpace α}, MeasurableSet s → s.Nonempty → ∃ f, Measurable f ∧ ∀ (x : ↑s), f ↑x = x
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>self : α ≃ᵐ β<GOAL>Measurable ⇑self.symm
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>self : α ≃ᵐ β<GOAL>Measurable ⇑self.toEquiv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<GOAL>Function.Injective MeasurableEquiv.toEquiv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<GOAL>⇑e.toEquiv = ⇑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<GOAL>Measurable ⇑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ β<VAR>h1 : Measurable ⇑e<VAR>h2 : Measurable ⇑e.symm<GOAL>⇑{ toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 } = ⇑e