Measurable.sup

theorem Measurable.sup : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f g : α → M} [inst_1 : Sup M] [inst_2 : MeasurableSup₂ M], Measurable f → Measurable g → Measurable fun a => f a ⊔ g a

This theorem, `Measurable.sup`, states that for any two functions `f` and `g` from a measurable space `α` to another measurable space `M` (equipped with a sup operation and a `MeasurableSup₂` instance), if both `f` and `g` are measurable, then the function that sends each element of `α` to the sup (or least upper bound) of the images of that element under `f` and `g`, is also measurable. In other words, the sup function preserves measurability.

More concisely: If `f` and `g` are measurable functions from a measurable space `α` to a measurable space `(M, ⊔)`, then the function that maps each `x ∈ α` to `⊔(f x, g x)` is also measurable.