α : Type u_1
β : Type ?u.1823883
γ : Type ?u.1823886
δ : Type ?u.1823889
m m0 : MeasurableSpace α
E : Type ?u.1823898
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : ℕ → Set α := spanningSets (Measure.trim μ hm)
⊢ f univ ≤ C
α : Type u_1
β : Type ?u.1823883
γ : Type ?u.1823886
δ : Type ?u.1823889
m m0 : MeasurableSpace α
E : Type ?u.1823898
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
⊢ f univ ≤ C
let S := @spanningSets _ m (μ.trim hm) _
α : Type u_1
β : Type ?u.1823883
γ : Type ?u.1823886
δ : Type ?u.1823889
m m0 : MeasurableSpace α
E : Type ?u.1823898
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : ℕ → Set α := spanningSets (Measure.trim μ hm)
hS_mono : Monotone S
⊢ f univ ≤ C
α : Type u_1
β : Type ?u.1823883
γ : Type ?u.1823886
δ : Type ?u.1823889
m m0 : MeasurableSpace α
E : Type ?u.1823898
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : ℕ → Set α := spanningSets (Measure.trim μ hm)
⊢ f univ ≤ C
have hS_mono : Monotone S := @monotone_spanningSets _ m (μ.trim hm) _
α : Type u_1
β : Type ?u.1823883
γ : Type ?u.1823886
δ : Type ?u.1823889
m m0 : MeasurableSpace α
E : Type ?u.1823898
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : ℕ → Set α := spanningSets (Measure.trim μ hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
⊢ f univ ≤ C
α : Type u_1
β : Type ?u.1823883
γ : Type ?u.1823886
δ : Type ?u.1823889
m m0 : MeasurableSpace α
E : Type ?u.1823898
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : ℕ → Set α := spanningSets (Measure.trim μ hm)
hS_mono : Monotone S
⊢ f univ ≤ C
have hS_meas : ∀ n, MeasurableSet[m] (S n) := @measurable_spanningSets _ m (μ.trim hm) _
α : Type u_1
β : Type ?u.1823883
γ : Type ?u.1823886
δ : Type ?u.1823889
m m0 : MeasurableSpace α
E : Type ?u.1823898
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : ℕ → Set α := spanningSets (Measure.trim μ hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
⊢ f (⋃ (i : ℕ), spanningSets (Measure.trim μ hm) i) ≤ C
α : Type u_1
β : Type ?u.1823883
γ : Type ?u.1823886
δ : Type ?u.1823889
m m0 : MeasurableSpace α
E : Type ?u.1823898
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : ℕ → Set α := spanningSets (Measure.trim μ hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
⊢ f univ ≤ C
rw [← @iUnion_spanningSets _ m (μ.trim hm)]
α : Type u_1
β : Type ?u.1823883
γ : Type ?u.1823886
δ : Type ?u.1823889
m m0 : MeasurableSpace α
E : Type ?u.1823898
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : ℕ → Set α := spanningSets (Measure.trim μ hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
⊢ (⨆ (n : ℕ), f (S n)) ≤ C
α : Type u_1
β : Type ?u.1823883
γ : Type ?u.1823886
δ : Type ?u.1823889
m m0 : MeasurableSpace α
E : Type ?u.1823898
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : ℕ → Set α := spanningSets (Measure.trim μ hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
⊢ f (⋃ (i : ℕ), spanningSets (Measure.trim μ hm) i) ≤ C
refine' (h_F_lim S hS_meas hS_mono).trans _
α : Type u_1
β : Type ?u.1823883
γ : Type ?u.1823886
δ : Type ?u.1823889
m m0 : MeasurableSpace α
E : Type ?u.1823898
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : ℕ → Set α := spanningSets (Measure.trim μ hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
n : ℕ
⊢ ↑↑μ (S n) ≠ ⊤
α : Type u_1
β : Type ?u.1823883
γ : Type ?u.1823886
δ : Type ?u.1823889
m m0 : MeasurableSpace α
E : Type ?u.1823898
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : ℕ → Set α := spanningSets (Measure.trim μ hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
⊢ (⨆ (n : ℕ), f (S n)) ≤ C
refine' iSup_le fun n => hf (S n) (hS_meas n) _
no goals
α : Type u_1
β : Type ?u.1823883
γ : Type ?u.1823886
δ : Type ?u.1823889
m m0 : MeasurableSpace α
E : Type ?u.1823898
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)
S : ℕ → Set α := spanningSets (Measure.trim μ hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
n : ℕ
⊢ ↑↑μ (S n) ≠ ⊤
exact ((le_trim hm).trans_lt (@measure_spanningSets_lt_top _ m (μ.trim hm) _ n)).ne