measurable_max🔗

This page has the declaration's own card below, then its dependency graph, then a card for each dependency (type dependencies first, then the rest of the transitive closure). For a theorem, the graph and the dependency cards only follow its statement's dependencies (its proof is replaced by sorry, so what it proves doesn't depend on how); for everything else, both the type and the body/value are followed, since their content is part of what later declarations build on.

Minimal Lean file

measurable_max.{u_1, u_2} {ι : Type u_1} {α : Type u_2} [LinearOrder α]
  [Fintype ι] [Nonempty ι] [MeasurableSpace α] [MeasurableSup₂ α] :
  Measurable fun t => Function.max t
measurable_max.{u_1, u_2} {ι : Type u_1}
  {α : Type u_2} [LinearOrder α]
  [Fintype ι] [Nonempty ι]
  [MeasurableSpace α] [MeasurableSup₂ α] :
  Measurable fun t => Function.max t

lemma measurable_max [MeasurableSup₂ α] : Measurable (fun (t : ι → α) => t.max)

fun_prop)]
lemma measurable_max [MeasurableSup₂ α] : Measurable (fun (t : ι → α) => t.max) := by
  suffices (fun f : ι → α ↦ f.max) = (univ.sup' univ_nonempty fun i f => f i) by
    rw [this]
    exact measurable_sup' univ_nonempty (fun i _ => measurable_pi_apply i)
  ext
  simp [Function.max]

Dependency graph

Type dependencies (1)

Function.max.{u_1, u_2} {ι : Type u_1} {α : Type u_2} [LinearOrder α]
  [Fintype ι] [Nonempty ι] (f : ι → α) : α
Function.max.{u_1, u_2} {ι : Type u_1}
  {α : Type u_2} [LinearOrder α]
  [Fintype ι] [Nonempty ι] (f : ι → α) : α

abbrev max : α := univ.sup' univ_nonempty f