α : Type u_1
β : Type ?u.3500690
γ : Type ?u.3500693
δ : Type ?u.3500696
ι : Type ?u.3500699
R : Type ?u.3500702
R' : Type ?u.3500705
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ IsFiniteMeasure (trim μ (_ : ⊥ ≤ m0)) ↔ IsFiniteMeasure μ
α : Type u_1
β : Type ?u.3500690
γ : Type ?u.3500693
δ : Type ?u.3500696
ι : Type ?u.3500699
R : Type ?u.3500702
R' : Type ?u.3500705
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ SigmaFinite (trim μ (_ : ⊥ ≤ m0)) ↔ IsFiniteMeasure μ
rw [sigmaFinite_bot_iff]
case refine'_1
α : Type u_1
β : Type ?u.3500690
γ : Type ?u.3500693
δ : Type ?u.3500696
ι : Type ?u.3500699
R : Type ?u.3500702
R' : Type ?u.3500705
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsFiniteMeasure (trim μ (_ : ⊥ ≤ m0))
h_univ : ↑↑(trim μ (_ : ⊥ ≤ m0)) univ < ⊤
⊢ ↑↑μ univ < ⊤

case refine'_2
α : Type u_1
β : Type ?u.3500690
γ : Type ?u.3500693
δ : Type ?u.3500696
ι : Type ?u.3500699
R : Type ?u.3500702
R' : Type ?u.3500705
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsFiniteMeasure μ
h_univ : ↑↑μ univ < ⊤
⊢ ↑↑(trim μ (_ : ⊥ ≤ m0)) univ < ⊤
α : Type u_1
β : Type ?u.3500690
γ : Type ?u.3500693
δ : Type ?u.3500696
ι : Type ?u.3500699
R : Type ?u.3500702
R' : Type ?u.3500705
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ IsFiniteMeasure (trim μ (_ : ⊥ ≤ m0)) ↔ IsFiniteMeasure μ
refine' ⟨fun h => ⟨_⟩, fun h => ⟨_⟩⟩ <;> have h_univ := h.measure_univ_lt_top
no goals
case refine'_1
α : Type u_1
β : Type ?u.3500690
γ : Type ?u.3500693
δ : Type ?u.3500696
ι : Type ?u.3500699
R : Type ?u.3500702
R' : Type ?u.3500705
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsFiniteMeasure (trim μ (_ : ⊥ ≤ m0))
h_univ : ↑↑(trim μ (_ : ⊥ ≤ m0)) univ < ⊤
⊢ ↑↑μ univ < ⊤
rwa [trim_measurableSet_eq bot_le MeasurableSet.univ] at h_univ
no goals
case refine'_2
α : Type u_1
β : Type ?u.3500690
γ : Type ?u.3500693
δ : Type ?u.3500696
ι : Type ?u.3500699
R : Type ?u.3500702
R' : Type ?u.3500705
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsFiniteMeasure μ
h_univ : ↑↑μ univ < ⊤
⊢ ↑↑(trim μ (_ : ⊥ ≤ m0)) univ < ⊤
rwa [trim_measurableSet_eq bot_le MeasurableSet.univ]