LeanMachineLearning exposition

1.5. ForMathlib.MeasureTheory.Order.Lattice🔗

Measurable inf of a finite set

Module LeanMachineLearning.ForMathlib.MeasureTheory.Order.Lattice contains 1 exposed declarations.

measurable_inf'🔗

TheoremFinset.measurable_inf'
Details

Dual version of Finset.measurable_sup'.

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

Code

theorem Finset.measurable_inf' {ι : Type*} {s : Finset ι} (hs : s.Nonempty) {f : ι → δ → α}
    (hf : ∀ n ∈ s, Measurable (f n)) : Measurable (s.inf' hs f)
Used by (1)

Actions: Source · Open Issue

Proof
fun_prop)]
theorem Finset.measurable_inf' {ι : Type*} {s : Finset ι} (hs : s.Nonempty) {f : ι → δ → α}
    (hf : ∀ n ∈ s, Measurable (f n)) : Measurable (s.inf' hs f) :=
  Finset.inf'_induction hs _ (fun _f hf _g hg => hf.inf hg) fun n hn => hf n hn
  1. Finset.measurable_inf'