ι✝ : Type ?u.6064426
ι' : Type ?u.6064429
α✝ : ι✝ → Type ?u.6064434
inst✝¹ : Fintype ι✝
m✝ : (i : ι✝) → OuterMeasure (α✝ i)
ι : Type u
α : ι → Type v
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
⊢ MeasurePreserving ↑e
ι✝ : Type ?u.6064426
ι' : Type ?u.6064429
α✝ : ι✝ → Type ?u.6064434
inst✝¹ : Fintype ι✝
m✝ : (i : ι✝) → OuterMeasure (α✝ i)
ι : Type u
α : ι → Type v
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ MeasurePreserving ↑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit)
set e := MeasurableEquiv.ofUniqueOfUnique (∀ i, α i) Unit
ι✝ : Type ?u.6064426
ι' : Type ?u.6064429
α✝ : ι✝ → Type ?u.6064434
inst✝¹ : Fintype ι✝
m✝ : (i : ι✝) → OuterMeasure (α✝ i)
ι : Type u
α : ι → Type v
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
⊢ Measure.map (↑e) (Measure.pi μ) = Measure.dirac ()
ι✝ : Type ?u.6064426
ι' : Type ?u.6064429
α✝ : ι✝ → Type ?u.6064434
inst✝¹ : Fintype ι✝
m✝ : (i : ι✝) → OuterMeasure (α✝ i)
ι : Type u
α : ι → Type v
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
⊢ MeasurePreserving ↑e
refine' ⟨e.measurable, _⟩
no goals
ι✝ : Type ?u.6064426
ι' : Type ?u.6064429
α✝ : ι✝ → Type ?u.6064434
inst✝¹ : Fintype ι✝
m✝ : (i : ι✝) → OuterMeasure (α✝ i)
ι : Type u
α : ι → Type v
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
⊢ Measure.map (↑e) (Measure.pi μ) = Measure.dirac ()
rw [Measure.pi_of_empty, Measure.map_dirac e.measurable]