case measure_univ
α : Type u_1
β : Type ?u.654181
γ : Type ?u.654184
δ : Type ?u.654187
ι : Type ?u.654190
R : Type ?u.654193
R' : Type ?u.654196
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsFiniteMeasure μ
h : μ ≠ 0
⊢ ↑↑((↑↑μ univ)⁻¹ • μ) univ = 1
α : Type u_1
β : Type ?u.654181
γ : Type ?u.654184
δ : Type ?u.654187
ι : Type ?u.654190
R : Type ?u.654193
R' : Type ?u.654196
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsFiniteMeasure μ
h : μ ≠ 0
⊢ IsProbabilityMeasure ((↑↑μ univ)⁻¹ • μ)
constructor
case measure_univ.h0
α : Type u_1
β : Type ?u.654181
γ : Type ?u.654184
δ : Type ?u.654187
ι : Type ?u.654190
R : Type ?u.654193
R' : Type ?u.654196
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsFiniteMeasure μ
h : μ ≠ 0
⊢ ↑↑μ univ ≠ 0

case measure_univ.ht
α : Type u_1
β : Type ?u.654181
γ : Type ?u.654184
δ : Type ?u.654187
ι : Type ?u.654190
R : Type ?u.654193
R' : Type ?u.654196
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsFiniteMeasure μ
h : μ ≠ 0
⊢ ↑↑μ univ ≠ ⊤
case measure_univ
α : Type u_1
β : Type ?u.654181
γ : Type ?u.654184
δ : Type ?u.654187
ι : Type ?u.654190
R : Type ?u.654193
R' : Type ?u.654196
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsFiniteMeasure μ
h : μ ≠ 0
⊢ ↑↑((↑↑μ univ)⁻¹ • μ) univ = 1
rw [smul_apply, smul_eq_mul, ENNReal.inv_mul_cancel]
no goals
case measure_univ.h0
α : Type u_1
β : Type ?u.654181
γ : Type ?u.654184
δ : Type ?u.654187
ι : Type ?u.654190
R : Type ?u.654193
R' : Type ?u.654196
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsFiniteMeasure μ
h : μ ≠ 0
⊢ ↑↑μ univ ≠ 0
rwa [Ne, measure_univ_eq_zero]
no goals
case measure_univ.ht
α : Type u_1
β : Type ?u.654181
γ : Type ?u.654184
δ : Type ?u.654187
ι : Type ?u.654190
R : Type ?u.654193
R' : Type ?u.654196
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsFiniteMeasure μ
h : μ ≠ 0
⊢ ↑↑μ univ ≠ ⊤
exact measure_ne_top _ _