Measurable inf of a finite set

theorem Finset.measurable_inf' {α : Type u_1} {δ : Type u_2} [MeasurableSpace δ] [SemilatticeInf α] {m : MeasurableSpace α} [MeasurableInf₂ α] {ι : Type u_3} {s : Finset ι} (hs : s.Nonempty) {f : ι → δ → α} (hf : ∀ n ∈ s, Measurable (f n)) : Measurable (s.inf' hs f)

Dual version of Finset.measurable_sup'.