α : Type u_1
β : Type ?u.75562
γ : Type ?u.75565
δ : Type ?u.75568
ι : Type ?u.75571
R : Type ?u.75574
R' : Type ?u.75577
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), ↑↑μ (s n \ t) = 0 ∧ ↑↑μ (t \ s n) = 0
⊢ ↑↑μ (limsup s atTop \ t) = 0 ∧ ↑↑μ (t \ limsup s atTop) = 0
α : Type u_1
β : Type ?u.75562
γ : Type ?u.75565
δ : Type ?u.75568
ι : Type ?u.75571
R : Type ?u.75574
R' : Type ?u.75577
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), s n =ᵐ[μ] t
⊢ limsup s atTop =ᵐ[μ] t
simp_rw [ae_eq_set] at h⊢
case left
α : Type u_1
β : Type ?u.75562
γ : Type ?u.75565
δ : Type ?u.75568
ι : Type ?u.75571
R : Type ?u.75574
R' : Type ?u.75577
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), ↑↑μ (s n \ t) = 0 ∧ ↑↑μ (t \ s n) = 0
⊢ ↑↑μ (limsup s atTop \ t) = 0

case right
α : Type u_1
β : Type ?u.75562
γ : Type ?u.75565
δ : Type ?u.75568
ι : Type ?u.75571
R : Type ?u.75574
R' : Type ?u.75577
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), ↑↑μ (s n \ t) = 0 ∧ ↑↑μ (t \ s n) = 0
⊢ ↑↑μ (t \ limsup s atTop) = 0
α : Type u_1
β : Type ?u.75562
γ : Type ?u.75565
δ : Type ?u.75568
ι : Type ?u.75571
R : Type ?u.75574
R' : Type ?u.75577
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), ↑↑μ (s n \ t) = 0 ∧ ↑↑μ (t \ s n) = 0
⊢ ↑↑μ (limsup s atTop \ t) = 0 ∧ ↑↑μ (t \ limsup s atTop) = 0
constructor
case left
α : Type u_1
β : Type ?u.75562
γ : Type ?u.75565
δ : Type ?u.75568
ι : Type ?u.75571
R : Type ?u.75574
R' : Type ?u.75577
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), ↑↑μ (s n \ t) = 0 ∧ ↑↑μ (t \ s n) = 0
⊢ ↑↑μ (limsup (fun b => s b \ t) atTop) = 0
case left
α : Type u_1
β : Type ?u.75562
γ : Type ?u.75565
δ : Type ?u.75568
ι : Type ?u.75571
R : Type ?u.75574
R' : Type ?u.75577
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), ↑↑μ (s n \ t) = 0 ∧ ↑↑μ (t \ s n) = 0
⊢ ↑↑μ (limsup s atTop \ t) = 0
rw [atTop.limsup_sdiff s t]
case left.hs
α : Type u_1
β : Type ?u.75562
γ : Type ?u.75565
δ : Type ?u.75568
ι : Type ?u.75571
R : Type ?u.75574
R' : Type ?u.75577
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), ↑↑μ (s n \ t) = 0 ∧ ↑↑μ (t \ s n) = 0
⊢ (∑' (i : ℕ), ↑↑μ (s i \ t)) ≠ ⊤
case left
α : Type u_1
β : Type ?u.75562
γ : Type ?u.75565
δ : Type ?u.75568
ι : Type ?u.75571
R : Type ?u.75574
R' : Type ?u.75577
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), ↑↑μ (s n \ t) = 0 ∧ ↑↑μ (t \ s n) = 0
⊢ ↑↑μ (limsup (fun b => s b \ t) atTop) = 0
apply measure_limsup_eq_zero
no goals
case left.hs
α : Type u_1
β : Type ?u.75562
γ : Type ?u.75565
δ : Type ?u.75568
ι : Type ?u.75571
R : Type ?u.75574
R' : Type ?u.75577
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), ↑↑μ (s n \ t) = 0 ∧ ↑↑μ (t \ s n) = 0
⊢ (∑' (i : ℕ), ↑↑μ (s i \ t)) ≠ ⊤
simp [h]
case right
α : Type u_1
β : Type ?u.75562
γ : Type ?u.75565
δ : Type ?u.75568
ι : Type ?u.75571
R : Type ?u.75574
R' : Type ?u.75577
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), ↑↑μ (s n \ t) = 0 ∧ ↑↑μ (t \ s n) = 0
⊢ ↑↑μ (liminf (fun b => t \ s b) atTop) = 0
case right
α : Type u_1
β : Type ?u.75562
γ : Type ?u.75565
δ : Type ?u.75568
ι : Type ?u.75571
R : Type ?u.75574
R' : Type ?u.75577
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), ↑↑μ (s n \ t) = 0 ∧ ↑↑μ (t \ s n) = 0
⊢ ↑↑μ (t \ limsup s atTop) = 0
rw [atTop.sdiff_limsup s t]
case right.h
α : Type u_1
β : Type ?u.75562
γ : Type ?u.75565
δ : Type ?u.75568
ι : Type ?u.75571
R : Type ?u.75574
R' : Type ?u.75577
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), ↑↑μ (s n \ t) = 0 ∧ ↑↑μ (t \ s n) = 0
⊢ (∑' (i : ℕ), ↑↑μ (t \ s i)) ≠ ⊤
case right
α : Type u_1
β : Type ?u.75562
γ : Type ?u.75565
δ : Type ?u.75568
ι : Type ?u.75571
R : Type ?u.75574
R' : Type ?u.75577
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), ↑↑μ (s n \ t) = 0 ∧ ↑↑μ (t \ s n) = 0
⊢ ↑↑μ (liminf (fun b => t \ s b) atTop) = 0
apply measure_liminf_eq_zero
no goals
case right.h
α : Type u_1
β : Type ?u.75562
γ : Type ?u.75565
δ : Type ?u.75568
ι : Type ?u.75571
R : Type ?u.75574
R' : Type ?u.75577
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), ↑↑μ (s n \ t) = 0 ∧ ↑↑μ (t \ s n) = 0
⊢ (∑' (i : ℕ), ↑↑μ (t \ s i)) ≠ ⊤
simp [h]