α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
⊢ ∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ ↑↑μ (s n) < ⊤ ∧ ∀ (x : α), x ∈ s n → ‖f x‖ ≤ ↑n) ∧ (⋃ (i : ℕ), s i) = univ
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
⊢ ∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ ↑↑μ (s n) < ⊤ ∧ ∀ (x : α), x ∈ s n → ‖f x‖ ≤ ↑n) ∧ (⋃ (i : ℕ), s i) = univ
let sigma_finite_sets := spanningSets (μ.trim hm)
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
⊢ ∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ ↑↑μ (s n) < ⊤ ∧ ∀ (x : α), x ∈ s n → ‖f x‖ ≤ ↑n) ∧ (⋃ (i : ℕ), s i) = univ
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
⊢ ∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ ↑↑μ (s n) < ⊤ ∧ ∀ (x : α), x ∈ s n → ‖f x‖ ≤ ↑n) ∧ (⋃ (i : ℕ), s i) = univ
let norm_sets := fun n : ℕ => { x | ‖f x‖ ≤ n }
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
⊢ ∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ ↑↑μ (s n) < ⊤ ∧ ∀ (x : α), x ∈ s n → ‖f x‖ ≤ ↑n) ∧ (⋃ (i : ℕ), s i) = univ
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
⊢ ∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ ↑↑μ (s n) < ⊤ ∧ ∀ (x : α), x ∈ s n → ‖f x‖ ≤ ↑n) ∧ (⋃ (i : ℕ), s i) = univ
have norm_sets_spanning : (⋃ n, norm_sets n) = Set.univ := by
  ext1 x
  simp only [Set.mem_iUnion, Set.mem_setOf_eq, Set.mem_univ, iff_true_iff]
  exact ⟨⌈‖f x‖⌉₊, Nat.le_ceil ‖f x‖⟩
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
⊢ ∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ ↑↑μ (s n) < ⊤ ∧ ∀ (x : α), x ∈ s n → ‖f x‖ ≤ ↑n) ∧ (⋃ (i : ℕ), s i) = univ
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
⊢ ∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ ↑↑μ (s n) < ⊤ ∧ ∀ (x : α), x ∈ s n → ‖f x‖ ≤ ↑n) ∧ (⋃ (i : ℕ), s i) = univ
let sets n := sigma_finite_sets n ∩ norm_sets n
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
⊢ ∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ ↑↑μ (s n) < ⊤ ∧ ∀ (x : α), x ∈ s n → ‖f x‖ ≤ ↑n) ∧ (⋃ (i : ℕ), s i) = univ
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
⊢ ∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ ↑↑μ (s n) < ⊤ ∧ ∀ (x : α), x ∈ s n → ‖f x‖ ≤ ↑n) ∧ (⋃ (i : ℕ), s i) = univ
have h_finite : ∀ n, μ (sets n) < ∞ := by
  refine' fun n => (measure_mono (Set.inter_subset_left _ _)).trans_lt _
  exact (le_trim hm).trans_lt (measure_spanningSets_lt_top (μ.trim hm) n)
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
n : ℕ
⊢ ∀ (x : α), x ∈ sets n → ‖f x‖ ≤ ↑n

case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
⊢ (⋃ (i : ℕ), sets i) = univ
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
⊢ ∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ ↑↑μ (s n) < ⊤ ∧ ∀ (x : α), x ∈ s n → ‖f x‖ ≤ ↑n) ∧ (⋃ (i : ℕ), s i) = univ
refine' ⟨sets, fun n => ⟨h_meas n, h_finite n, _⟩, _⟩
case h
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
x : α
⊢ (x ∈ ⋃ (n : ℕ), norm_sets n) ↔ x ∈ univ
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
⊢ (⋃ (n : ℕ), norm_sets n) = univ
ext1 x
case h
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
x : α
⊢ ∃ i, ‖f x‖ ≤ ↑i
case h
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
x : α
⊢ (x ∈ ⋃ (n : ℕ), norm_sets n) ↔ x ∈ univ
simp only [Set.mem_iUnion, Set.mem_setOf_eq, Set.mem_univ, iff_true_iff]
no goals
case h
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
x : α
⊢ ∃ i, ‖f x‖ ≤ ↑i
exact ⟨⌈‖f x‖⌉₊, Nat.le_ceil ‖f x‖⟩
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
n : ℕ
⊢ MeasurableSet (sigma_finite_sets n)

case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
n : ℕ
⊢ MeasurableSet (norm_sets n)
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
⊢ ∀ (n : ℕ), MeasurableSet (sets n)
refine' fun n => MeasurableSet.inter _ _
no goals
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
n : ℕ
⊢ MeasurableSet (sigma_finite_sets n)
exact measurable_spanningSets (μ.trim hm) n
no goals
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
n : ℕ
⊢ MeasurableSet (norm_sets n)
exact hf.norm.measurableSet_le stronglyMeasurable_const
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
n : ℕ
⊢ ↑↑μ (sigma_finite_sets n) < ⊤
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
⊢ ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
refine' fun n => (measure_mono (Set.inter_subset_left _ _)).trans_lt _
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
n : ℕ
⊢ ↑↑μ (sigma_finite_sets n) < ⊤
exact (le_trim hm).trans_lt (measure_spanningSets_lt_top (μ.trim hm) n)
no goals
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
n : ℕ
⊢ ∀ (x : α), x ∈ sets n → ‖f x‖ ≤ ↑n
exact fun x hx => hx.2
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
this : (⋃ (i : ℕ), sigma_finite_sets i ∩ norm_sets i) = (⋃ (i : ℕ), sigma_finite_sets i) ∩ ⋃ (i : ℕ), norm_sets i
⊢ (⋃ (i : ℕ), sets i) = univ
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
⊢ (⋃ (i : ℕ), sets i) = univ
have :
  (⋃ i, sigma_finite_sets i ∩ norm_sets i) = (⋃ i, sigma_finite_sets i) ∩ ⋃ i, norm_sets i := by
  refine' Set.iUnion_inter_of_monotone (monotone_spanningSets (μ.trim hm)) fun i j hij x => _
  simp only [Set.mem_setOf_eq]
  refine' fun hif => hif.trans _
  exact_mod_cast hij
no goals
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
this : (⋃ (i : ℕ), sigma_finite_sets i ∩ norm_sets i) = (⋃ (i : ℕ), sigma_finite_sets i) ∩ ⋃ (i : ℕ), norm_sets i
⊢ (⋃ (i : ℕ), sets i) = univ
rw [this, norm_sets_spanning, iUnion_spanningSets (μ.trim hm), Set.inter_univ]
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
i j : ℕ
hij : i ≤ j
x : α
⊢ x ∈ norm_sets i → x ∈ norm_sets j
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
⊢ (⋃ (i : ℕ), sigma_finite_sets i ∩ norm_sets i) = (⋃ (i : ℕ), sigma_finite_sets i) ∩ ⋃ (i : ℕ), norm_sets i
refine' Set.iUnion_inter_of_monotone (monotone_spanningSets (μ.trim hm)) fun i j hij x => _
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
i j : ℕ
hij : i ≤ j
x : α
⊢ ‖f x‖ ≤ ↑i → ‖f x‖ ≤ ↑j
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
i j : ℕ
hij : i ≤ j
x : α
⊢ x ∈ norm_sets i → x ∈ norm_sets j
simp only [Set.mem_setOf_eq]
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
i j : ℕ
hij : i ≤ j
x : α
hif : ‖f x‖ ≤ ↑i
⊢ ↑i ≤ ↑j
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
i j : ℕ
hij : i ≤ j
x : α
⊢ ‖f x‖ ≤ ↑i → ‖f x‖ ≤ ↑j
refine' fun hif => hif.trans _
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.233047
ι : Type ?u.233050
inst✝² : Countable ι
f g : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (trim μ hm)
sigma_finite_sets : ℕ → Set α := spanningSets (trim μ hm)
norm_sets : ℕ → Set α := fun n => {x | ‖f x‖ ≤ ↑n}
norm_sets_spanning : (⋃ (n : ℕ), norm_sets n) = univ
sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), ↑↑μ (sets n) < ⊤
i j : ℕ
hij : i ≤ j
x : α
hif : ‖f x‖ ≤ ↑i
⊢ ↑i ≤ ↑j
exact_mod_cast hij