case mp
α : Type u_1
β : Type ?u.3868099
γ : Type ?u.3868102
δ : Type ?u.3868105
ι : Type ?u.3868108
R : Type ?u.3868111
R' : Type ?u.3868114
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : CompactSpace α
a✝ : IsFiniteMeasure μ
⊢ IsFiniteMeasureOnCompacts μ

case mpr
α : Type u_1
β : Type ?u.3868099
γ : Type ?u.3868102
δ : Type ?u.3868105
ι : Type ?u.3868108
R : Type ?u.3868111
R' : Type ?u.3868114
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : CompactSpace α
a✝ : IsFiniteMeasureOnCompacts μ
⊢ IsFiniteMeasure μ
α : Type u_1
β : Type ?u.3868099
γ : Type ?u.3868102
δ : Type ?u.3868105
ι : Type ?u.3868108
R : Type ?u.3868111
R' : Type ?u.3868114
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : CompactSpace α
⊢ IsFiniteMeasure μ ↔ IsFiniteMeasureOnCompacts μ
constructor <;> intros
no goals
case mp
α : Type u_1
β : Type ?u.3868099
γ : Type ?u.3868102
δ : Type ?u.3868105
ι : Type ?u.3868108
R : Type ?u.3868111
R' : Type ?u.3868114
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : CompactSpace α
a✝ : IsFiniteMeasure μ
⊢ IsFiniteMeasureOnCompacts μ
infer_instance
no goals
case mpr
α : Type u_1
β : Type ?u.3868099
γ : Type ?u.3868102
δ : Type ?u.3868105
ι : Type ?u.3868108
R : Type ?u.3868111
R' : Type ?u.3868114
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : CompactSpace α
a✝ : IsFiniteMeasureOnCompacts μ
⊢ IsFiniteMeasure μ
exact CompactSpace.isFiniteMeasure