ι : Type ?u.5846526
ι' : Type ?u.5846529
α✝ : ι → Type ?u.5846534
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
⊢ MeasurePreserving ↑e
ι : Type ?u.5846526
ι' : Type ?u.5846529
α✝ : ι → Type ?u.5846534
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
⊢ MeasurePreserving ↑(MeasurableEquiv.funUnique α β)
set e := MeasurableEquiv.funUnique α β
ι : Type ?u.5846526
ι' : Type ?u.5846529
α✝ : ι → Type ?u.5846534
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
this : (piPremeasure fun x => ↑μ) = ↑↑(Measure.map (↑(MeasurableEquiv.symm e)) μ)
⊢ MeasurePreserving ↑e
ι : Type ?u.5846526
ι' : Type ?u.5846529
α✝ : ι → Type ?u.5846534
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
⊢ MeasurePreserving ↑e
have : (piPremeasure fun _ : α => μ.toOuterMeasure) = Measure.map e.symm μ := by
  ext1 s
  rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply]
  congr 1; exact e.toEquiv.image_eq_preimage s
ι : Type ?u.5846526
ι' : Type ?u.5846529
α✝ : ι → Type ?u.5846534
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
this : (piPremeasure fun x => ↑μ) = ↑↑(Measure.map (↑(MeasurableEquiv.symm e)) μ)
⊢ MeasurePreserving ↑(MeasurableEquiv.funUnique α β)
ι : Type ?u.5846526
ι' : Type ?u.5846529
α✝ : ι → Type ?u.5846534
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
this : (piPremeasure fun x => ↑μ) = ↑↑(Measure.map (↑(MeasurableEquiv.symm e)) μ)
⊢ MeasurePreserving ↑e
simp only [Measure.pi, OuterMeasure.pi, this, boundedBy_measure, toOuterMeasure_toMeasure]
no goals
ι : Type ?u.5846526
ι' : Type ?u.5846529
α✝ : ι → Type ?u.5846534
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
this : (piPremeasure fun x => ↑μ) = ↑↑(Measure.map (↑(MeasurableEquiv.symm e)) μ)
⊢ MeasurePreserving ↑(MeasurableEquiv.funUnique α β)
exact (e.symm.measurable.measurePreserving _).symm e.symm
case h
ι : Type ?u.5846526
ι' : Type ?u.5846529
α✝ : ι → Type ?u.5846534
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
s : Set (α → β)
⊢ piPremeasure (fun x => ↑μ) s = ↑↑(Measure.map (↑(MeasurableEquiv.symm e)) μ) s
ι : Type ?u.5846526
ι' : Type ?u.5846529
α✝ : ι → Type ?u.5846534
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
⊢ (piPremeasure fun x => ↑μ) = ↑↑(Measure.map (↑(MeasurableEquiv.symm e)) μ)
ext1 s
case h
ι : Type ?u.5846526
ι' : Type ?u.5846529
α✝ : ι → Type ?u.5846534
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
s : Set (α → β)
⊢ ↑↑μ (eval default '' s) = ↑↑μ (↑(MeasurableEquiv.symm e) ⁻¹' s)
case h
ι : Type ?u.5846526
ι' : Type ?u.5846529
α✝ : ι → Type ?u.5846534
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
s : Set (α → β)
⊢ piPremeasure (fun x => ↑μ) s = ↑↑(Measure.map (↑(MeasurableEquiv.symm e)) μ) s
rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply]
case h.e_a
ι : Type ?u.5846526
ι' : Type ?u.5846529
α✝ : ι → Type ?u.5846534
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
s : Set (α → β)
⊢ eval default '' s = ↑(MeasurableEquiv.symm e) ⁻¹' s
case h
ι : Type ?u.5846526
ι' : Type ?u.5846529
α✝ : ι → Type ?u.5846534
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
s : Set (α → β)
⊢ ↑↑μ (eval default '' s) = ↑↑μ (↑(MeasurableEquiv.symm e) ⁻¹' s)
congr 1
no goals
case h.e_a
ι : Type ?u.5846526
ι' : Type ?u.5846529
α✝ : ι → Type ?u.5846534
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
s : Set (α → β)
⊢ eval default '' s = ↑(MeasurableEquiv.symm e) ⁻¹' s
exact e.toEquiv.image_eq_preimage s