α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
⊢ ∃ x, ∀ (x_1 : ℝ), x_1 ∈ measureOfNegatives s → x ≤ x_1
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
⊢ BddBelow (measureOfNegatives s)
simp_rw [BddBelow, Set.Nonempty, mem_lowerBounds]
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
⊢ False
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
⊢ ∃ x, ∀ (x_1 : ℝ), x_1 ∈ measureOfNegatives s → x ≤ x_1
by_contra' h
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
h' : ∀ (n : ℕ), ∃ y, y ∈ measureOfNegatives s ∧ y < -↑n
⊢ False
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
⊢ False
have h' : ∀ n : ℕ, ∃ y : ℝ, y ∈ s.measureOfNegatives ∧ y < -n := fun n => h (-n)
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
⊢ False
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
h' : ∀ (n : ℕ), ∃ y, y ∈ measureOfNegatives s ∧ y < -↑n
⊢ False
choose f hf using h'
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
hf' : ∀ (n : ℕ), ∃ B, MeasurableSet B ∧ restrict s B ≤ restrict 0 B ∧ ↑s B < -↑n
⊢ False
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
⊢ False
have hf' : ∀ n : ℕ, ∃ B, MeasurableSet B ∧ s ≤[B] 0 ∧ s B < -n := by
  intro n
  rcases hf n with ⟨⟨B, ⟨hB₁, hBr⟩, hB₂⟩, hlt⟩
  exact ⟨B, hB₁, hBr, hB₂.symm ▸ hlt⟩
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
⊢ False
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
hf' : ∀ (n : ℕ), ∃ B, MeasurableSet B ∧ restrict s B ≤ restrict 0 B ∧ ↑s B < -↑n
⊢ False
choose B hmeas hr h_lt using hf'
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
⊢ False
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
⊢ False
set A := ⋃ n, B n with hA
case intro
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hfalse : ∀ (n : ℕ), ↑s A ≤ -↑n
n : ℕ
hn : -↑s A < ↑n
⊢ False
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hfalse : ∀ (n : ℕ), ↑s A ≤ -↑n
⊢ False
rcases exists_nat_gt (-s A) with ⟨n, hn⟩
no goals
case intro
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hfalse : ∀ (n : ℕ), ↑s A ≤ -↑n
n : ℕ
hn : -↑s A < ↑n
⊢ False
exact lt_irrefl _ ((neg_lt.1 hn).trans_le (hfalse n))
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
n : ℕ
⊢ ∃ B, MeasurableSet B ∧ restrict s B ≤ restrict 0 B ∧ ↑s B < -↑n
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
⊢ ∀ (n : ℕ), ∃ B, MeasurableSet B ∧ restrict s B ≤ restrict 0 B ∧ ↑s B < -↑n
intro n
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
n : ℕ
hlt : f n < -↑n
B : Set α
hB₂ : ↑s B = f n
hB₁ : MeasurableSet B
hBr : restrict s B ≤ restrict 0 B
⊢ ∃ B, MeasurableSet B ∧ restrict s B ≤ restrict 0 B ∧ ↑s B < -↑n
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
n : ℕ
⊢ ∃ B, MeasurableSet B ∧ restrict s B ≤ restrict 0 B ∧ ↑s B < -↑n
rcases hf n with ⟨⟨B, ⟨hB₁, hBr⟩, hB₂⟩, hlt⟩
no goals
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
n : ℕ
hlt : f n < -↑n
B : Set α
hB₂ : ↑s B = f n
hB₁ : MeasurableSet B
hBr : restrict s B ≤ restrict 0 B
⊢ ∃ B, MeasurableSet B ∧ restrict s B ≤ restrict 0 B ∧ ↑s B < -↑n
exact ⟨B, hB₁, hBr, hB₂.symm ▸ hlt⟩
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
⊢ ↑s A ≤ -↑n
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
⊢ ∀ (n : ℕ), ↑s A ≤ -↑n
intro n
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
⊢ ↑s A ≤ ↑s (B n)
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
⊢ ↑s A ≤ -↑n
refine' le_trans _ (le_of_lt (h_lt _))
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
⊢ ↑s ((⋃ (i : ℕ), B i) \ B n) + ↑s (B n) ≤ ↑s (B n)

α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
⊢ MeasurableSet ((⋃ (i : ℕ), B i) \ B n)
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
⊢ ↑s A ≤ ↑s (B n)
rw [hA, ← Set.diff_union_of_subset (Set.subset_iUnion _ n),
  of_union Set.disjoint_sdiff_left _ (hmeas n)]
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
⊢ ↑s ((⋃ (i : ℕ), B i) \ B n) ≤ 0
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
⊢ ↑s ((⋃ (i : ℕ), B i) \ B n) + ↑s (B n) ≤ ↑s (B n)
refine' add_le_of_nonpos_left _
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
this : restrict s A ≤ restrict 0 A
⊢ ↑s ((⋃ (i : ℕ), B i) \ B n) ≤ 0
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
⊢ ↑s ((⋃ (i : ℕ), B i) \ B n) ≤ 0
have : s ≤[A] 0 := restrict_le_restrict_iUnion _ _ hmeas hr
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
this : restrict s A ≤ restrict 0 A
⊢ MeasurableSet (⋃ (i : ℕ), B i)
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
this : restrict s A ≤ restrict 0 A
⊢ ↑s ((⋃ (i : ℕ), B i) \ B n) ≤ 0
refine' nonpos_of_restrict_le_zero _ (restrict_le_zero_subset _ _ (Set.diff_subset _ _) this)
no goals
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
this : restrict s A ≤ restrict 0 A
⊢ MeasurableSet (⋃ (i : ℕ), B i)
exact MeasurableSet.iUnion hmeas
no goals
α : Type u_1
β : Type ?u.101130
inst✝³ : MeasurableSpace α
M : Type ?u.101136
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
h : ∀ (x : ℝ), ∃ x_1, x_1 ∈ measureOfNegatives s ∧ x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ measureOfNegatives s ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
⊢ MeasurableSet ((⋃ (i : ℕ), B i) \ B n)
exact (MeasurableSet.iUnion hmeas).diff (hmeas n)