theorem MeasureTheory.nullMeasurableSet_sum {ι : Type u_1} {α : Type u_2} {x✝ : MeasurableSpace α} [Countable ι] {μ : ι → Measure α} {s : Set α} : NullMeasurableSet s (Measure.sum μ) ↔ ∀ (i : ι), NullMeasurableSet s (μ i)

instance MeasureTheory.Measure.instIsFiniteMeasureComap_sardMoreira {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} (μ : Measure β) (f : α → β) [IsFiniteMeasure μ] : IsFiniteMeasure (comap f μ)

theorem MeasureTheory.Measure.comap_sum_countable {ι : Type u_1} {α : Type u_2} {β : Type u_3} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} [Countable ι] {f : α → β} {μ : ι → Measure β} (hf : ∀ (i : ι) (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) (μ i)) : comap f (sum μ) = sum fun (i : ι) => comap f (μ i)

def MeasureTheory.Measure.FiniteSpanningSetsIn.comap {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {μ : Measure β} {T : Set (Set β)} (sets : μ.FiniteSpanningSetsIn T) {S : Set (Set α)} {f : α → β} (hf : Set.MapsTo (fun (x : Set β) => f ⁻¹' x) T S) (hmeas : ∀ (n : ℕ), MeasurableSet (f ⁻¹' sets.set n)) : (comap f μ).FiniteSpanningSetsIn S

Equations

• sets.comap hf hmeas = { set := fun (n : ℕ) => f ⁻¹' sets.set n, set_mem := ⋯, finite := ⋯, spanning := ⋯ }

theorem MeasureTheory.SigmaFinite.comap {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} (μ : Measure β) {f : α → β} (hf : Measurable f) [SigmaFinite μ] : SigmaFinite (Measure.comap f μ)

instance MeasureTheory.Measure.instSigmaFiniteSubtypeComap_sardMoreira {α : Type u_1} {x✝ : MeasurableSpace α} {p : α → Prop} {μ : Measure α} [SigmaFinite μ] : SigmaFinite (comap Subtype.val μ)

instance MeasureTheory.Measure.instSFiniteComap_sardMoreira {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} (μ : Measure β) [SFinite μ] (f : α → β) : SFinite (comap f μ)