α : Type u_1
β : Type ?u.758001
γ : Type ?u.758004
δ : Type ?u.758007
ι : Type ?u.758010
R : Type ?u.758013
R' : Type ?u.758016
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
S : Set (Set α)
hc : Set.Countable S
hμ : ∀ (s : Set α), s ∈ S → ↑↑μ s < ⊤
hU : ⋃₀ S = univ
⊢ ∃ s, (∀ (n : ℕ), ↑↑μ (s n) < ⊤) ∧ (⋃ (n : ℕ), s n) = univ

case intro.intro
α : Type u_1
β : Type ?u.758001
γ : Type ?u.758004
δ : Type ?u.758007
ι : Type ?u.758010
R : Type ?u.758013
R' : Type ?u.758016
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
S : Set (Set α)
hc : Set.Countable S
hμ✝ : ∀ (s : Set α), s ∈ S → ↑↑μ s < ⊤
hU : ⋃₀ S = univ
s : ℕ → Set α
hμ : ∀ (n : ℕ), ↑↑μ (s n) < ⊤
hs : (⋃ (n : ℕ), s n) = univ
⊢ SigmaFinite μ
α : Type u_1
β : Type ?u.758001
γ : Type ?u.758004
δ : Type ?u.758007
ι : Type ?u.758010
R : Type ?u.758013
R' : Type ?u.758016
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
S : Set (Set α)
hc : Set.Countable S
hμ : ∀ (s : Set α), s ∈ S → ↑↑μ s < ⊤
hU : ⋃₀ S = univ
⊢ SigmaFinite μ
obtain ⟨s, hμ, hs⟩ : ∃ s : ℕ → Set α, (∀ n, μ (s n) < ∞) ∧ (⋃ n, s n) = univ
case intro.intro
α : Type u_1
β : Type ?u.758001
γ : Type ?u.758004
δ : Type ?u.758007
ι : Type ?u.758010
R : Type ?u.758013
R' : Type ?u.758016
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
S : Set (Set α)
hc : Set.Countable S
hμ✝ : ∀ (s : Set α), s ∈ S → ↑↑μ s < ⊤
hU : ⋃₀ S = univ
s : ℕ → Set α
hμ : ∀ (n : ℕ), ↑↑μ (s n) < ⊤
hs : (⋃ (n : ℕ), s n) = univ
⊢ SigmaFinite μ
α : Type u_1
β : Type ?u.758001
γ : Type ?u.758004
δ : Type ?u.758007
ι : Type ?u.758010
R : Type ?u.758013
R' : Type ?u.758016
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
S : Set (Set α)
hc : Set.Countable S
hμ : ∀ (s : Set α), s ∈ S → ↑↑μ s < ⊤
hU : ⋃₀ S = univ
⊢ ∃ s, (∀ (n : ℕ), ↑↑μ (s n) < ⊤) ∧ (⋃ (n : ℕ), s n) = univ

case intro.intro
α : Type u_1
β : Type ?u.758001
γ : Type ?u.758004
δ : Type ?u.758007
ι : Type ?u.758010
R : Type ?u.758013
R' : Type ?u.758016
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
S : Set (Set α)
hc : Set.Countable S
hμ✝ : ∀ (s : Set α), s ∈ S → ↑↑μ s < ⊤
hU : ⋃₀ S = univ
s : ℕ → Set α
hμ : ∀ (n : ℕ), ↑↑μ (s n) < ⊤
hs : (⋃ (n : ℕ), s n) = univ
⊢ SigmaFinite μ
exact (@exists_seq_cover_iff_countable _ (fun x => μ x < ⊤) ⟨∅, by simp⟩).2 ⟨S, hc, hμ, hU⟩
no goals
case intro.intro
α : Type u_1
β : Type ?u.758001
γ : Type ?u.758004
δ : Type ?u.758007
ι : Type ?u.758010
R : Type ?u.758013
R' : Type ?u.758016
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
S : Set (Set α)
hc : Set.Countable S
hμ✝ : ∀ (s : Set α), s ∈ S → ↑↑μ s < ⊤
hU : ⋃₀ S = univ
s : ℕ → Set α
hμ : ∀ (n : ℕ), ↑↑μ (s n) < ⊤
hs : (⋃ (n : ℕ), s n) = univ
⊢ SigmaFinite μ
exact ⟨⟨⟨fun n => s n, fun _ => trivial, hμ, hs⟩⟩⟩
no goals
α : Type u_1
β : Type ?u.758001
γ : Type ?u.758004
δ : Type ?u.758007
ι : Type ?u.758010
R : Type ?u.758013
R' : Type ?u.758016
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
S : Set (Set α)
hc : Set.Countable S
hμ : ∀ (s : Set α), s ∈ S → ↑↑μ s < ⊤
hU : ⋃₀ S = univ
⊢ (fun x => ↑↑μ x < ⊤) ∅
simp