α : Type u_1
β : Type ?u.3994641
E : Type u_2
F : Type ?u.3994647
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤
α : Type u_1
β : Type ?u.3994641
E : Type u_2
F : Type ?u.3994647
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
inst✝ : NoAtoms μ
⊢ ↑↑μ {a} ≠ ⊤
rw [measure_singleton]
no goals
α : Type u_1
β : Type ?u.3994641
E : Type u_2
F : Type ?u.3994647
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤
exact ENNReal.zero_ne_top