α : Type u_1
β : Type ?u.604437
γ : Type ?u.604440
δ : Type ?u.604443
ι : Type ?u.604446
R : Type ?u.604449
R' : Type ?u.604452
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
h : ¬IsFiniteMeasure μ
⊢ ↑↑μ univ = ⊤
α : Type u_1
β : Type ?u.604437
γ : Type ?u.604440
δ : Type ?u.604443
ι : Type ?u.604446
R : Type ?u.604449
R' : Type ?u.604452
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ ¬IsFiniteMeasure μ ↔ ↑↑μ univ = ⊤
refine' ⟨fun h => _, fun h => fun h' => h'.measure_univ_lt_top.ne h⟩
α : Type u_1
β : Type ?u.604437
γ : Type ?u.604440
δ : Type ?u.604443
ι : Type ?u.604446
R : Type ?u.604449
R' : Type ?u.604452
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
h : ¬IsFiniteMeasure μ
h' : ¬↑↑μ univ = ⊤
⊢ False
α : Type u_1
β : Type ?u.604437
γ : Type ?u.604440
δ : Type ?u.604443
ι : Type ?u.604446
R : Type ?u.604449
R' : Type ?u.604452
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
h : ¬IsFiniteMeasure μ
⊢ ↑↑μ univ = ⊤
by_contra h'
no goals
α : Type u_1
β : Type ?u.604437
γ : Type ?u.604440
δ : Type ?u.604443
ι : Type ?u.604446
R : Type ?u.604449
R' : Type ?u.604452
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
h : ¬IsFiniteMeasure μ
h' : ¬↑↑μ univ = ⊤
⊢ False
exact h ⟨lt_top_iff_ne_top.mpr h'⟩