case h.e'_4.h
α : Type u_1
β : Type ?u.112015
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
x✝ : α
⊢ iSup (fun k => ⨆ (_ : k ≤ n), f k) x✝ = ⨆ (k : ℕ) (_ : k ≤ n), f k x✝
α : Type u_1
β : Type ?u.112015
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
⊢ (⨆ (k : ℕ) (_ : k ≤ n), f k) ∈ measurableLE μ ν
convert iSup_mem_measurableLE f hf n
case h.e'_4.h
α : Type u_1
β : Type ?u.112015
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
x✝ : α
x : ℝ≥0
⊢ x ∈ iSup (fun k => ⨆ (_ : k ≤ n), f k) x✝ ↔ x ∈ ⨆ (k : ℕ) (_ : k ≤ n), f k x✝
case h.e'_4.h
α : Type u_1
β : Type ?u.112015
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
x✝ : α
⊢ iSup (fun k => ⨆ (_ : k ≤ n), f k) x✝ = ⨆ (k : ℕ) (_ : k ≤ n), f k x✝
refine Option.ext fun x => ?_
no goals
case h.e'_4.h
α : Type u_1
β : Type ?u.112015
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
x✝ : α
x : ℝ≥0
⊢ x ∈ iSup (fun k => ⨆ (_ : k ≤ n), f k) x✝ ↔ x ∈ ⨆ (k : ℕ) (_ : k ≤ n), f k x✝
simp