α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ↑{ measureOf' := fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0,
          empty' := (_ : (if MeasurableSet ∅ then ↑v (f ⁻¹' ∅) else 0) = 0),
          not_measurable' := (_ : ∀ (i : Set β), ¬MeasurableSet i → (if MeasurableSet i then ↑v (f ⁻¹' i) else 0) = 0),
          m_iUnion' :=
            (_ :
              ∀ ⦃g : ℕ → Set β⦄,
                (∀ (i : ℕ), MeasurableSet (g i)) →
                  Pairwise (Disjoint on g) →
                    HasSum (fun i => (fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0) (g i))
                      ((fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0) (⋃ (i : ℕ), g i))) }
      s =
    ↑v (f ⁻¹' s)
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ↑(map v f) s = ↑v (f ⁻¹' s)
rw [map, dif_pos hf]
no goals
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ↑{ measureOf' := fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0,
          empty' := (_ : (if MeasurableSet ∅ then ↑v (f ⁻¹' ∅) else 0) = 0),
          not_measurable' := (_ : ∀ (i : Set β), ¬MeasurableSet i → (if MeasurableSet i then ↑v (f ⁻¹' i) else 0) = 0),
          m_iUnion' :=
            (_ :
              ∀ ⦃g : ℕ → Set β⦄,
                (∀ (i : ℕ), MeasurableSet (g i)) →
                  Pairwise (Disjoint on g) →
                    HasSum (fun i => (fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0) (g i))
                      ((fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0) (⋃ (i : ℕ), g i))) }
      s =
    ↑v (f ⁻¹' s)
exact if_pos hs