α : Type u_1
β : Type ?u.73864
γ : Type ?u.73867
δ : Type ?u.73870
ι : Type ?u.73873
R : Type ?u.73876
R' : Type ?u.73879
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : ℕ → Set α
h : (∑' (i : ℕ), ↑↑μ (s i)) ≠ ⊤
⊢ ↑↑μ (liminf s atTop) ≤ 0
α : Type u_1
β : Type ?u.73864
γ : Type ?u.73867
δ : Type ?u.73870
ι : Type ?u.73873
R : Type ?u.73876
R' : Type ?u.73879
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : ℕ → Set α
h : (∑' (i : ℕ), ↑↑μ (s i)) ≠ ⊤
⊢ ↑↑μ (liminf s atTop) = 0
rw [← le_zero_iff]
α : Type u_1
β : Type ?u.73864
γ : Type ?u.73867
δ : Type ?u.73870
ι : Type ?u.73873
R : Type ?u.73876
R' : Type ?u.73879
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : ℕ → Set α
h : (∑' (i : ℕ), ↑↑μ (s i)) ≠ ⊤
this : liminf s atTop ≤ limsup s atTop
⊢ ↑↑μ (liminf s atTop) ≤ 0
α : Type u_1
β : Type ?u.73864
γ : Type ?u.73867
δ : Type ?u.73870
ι : Type ?u.73873
R : Type ?u.73876
R' : Type ?u.73879
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : ℕ → Set α
h : (∑' (i : ℕ), ↑↑μ (s i)) ≠ ⊤
⊢ ↑↑μ (liminf s atTop) ≤ 0
have : liminf s atTop ≤ limsup s atTop :=
  liminf_le_limsup
    (by isBoundedDefault)
    (by isBoundedDefault)
no goals
α : Type u_1
β : Type ?u.73864
γ : Type ?u.73867
δ : Type ?u.73870
ι : Type ?u.73873
R : Type ?u.73876
R' : Type ?u.73879
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : ℕ → Set α
h : (∑' (i : ℕ), ↑↑μ (s i)) ≠ ⊤
this : liminf s atTop ≤ limsup s atTop
⊢ ↑↑μ (liminf s atTop) ≤ 0
exact (μ.mono this).trans (by simp [measure_limsup_eq_zero h])
no goals
α : Type u_1
β : Type ?u.73864
γ : Type ?u.73867
δ : Type ?u.73870
ι : Type ?u.73873
R : Type ?u.73876
R' : Type ?u.73879
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : ℕ → Set α
h : (∑' (i : ℕ), ↑↑μ (s i)) ≠ ⊤
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop s
isBoundedDefault
no goals
α : Type u_1
β : Type ?u.73864
γ : Type ?u.73867
δ : Type ?u.73870
ι : Type ?u.73873
R : Type ?u.73876
R' : Type ?u.73879
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : ℕ → Set α
h : (∑' (i : ℕ), ↑↑μ (s i)) ≠ ⊤
⊢ IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop s
isBoundedDefault
no goals
α : Type u_1
β : Type ?u.73864
γ : Type ?u.73867
δ : Type ?u.73870
ι : Type ?u.73873
R : Type ?u.73876
R' : Type ?u.73879
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : ℕ → Set α
h : (∑' (i : ℕ), ↑↑μ (s i)) ≠ ⊤
this : liminf s atTop ≤ limsup s atTop
⊢ ↑↑μ (limsup s atTop) ≤ 0
simp [measure_limsup_eq_zero h]