M : Type ?u.1408591
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f✝ g : α → M
δ : Type u_1
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k < Nat.succ n → Measurable (f k)
⊢ Measurable (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) f)
M : Type ?u.1408591
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f✝ g : α → M
δ : Type u_1
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k ≤ n → Measurable (f k)
⊢ Measurable (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) f)
simp_rw [← Nat.lt_succ_iff] at hf
M : Type ?u.1408591
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f✝ g : α → M
δ : Type u_1
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k < Nat.succ n → Measurable (f k)
⊢ ∀ (n_1 : ℕ), n_1 ∈ range (n + 1) → Measurable (f n_1)
M : Type ?u.1408591
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f✝ g : α → M
δ : Type u_1
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k < Nat.succ n → Measurable (f k)
⊢ Measurable (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) f)
refine' Finset.measurable_sup' _ _
no goals
M : Type ?u.1408591
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f✝ g : α → M
δ : Type u_1
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k < Nat.succ n → Measurable (f k)
⊢ ∀ (n_1 : ℕ), n_1 ∈ range (n + 1) → Measurable (f n_1)
simpa [Finset.mem_range]