English
Let M be a type equipped with a minimum operation ⊓ that makes it a lattice, and assume that the infimum operation is measurable in both arguments. If f,g: α → M are measurable, then the pointwise infimum a ↦ f(a) ⊓ g(a) is measurable.
Русский
Пусть M — множество с операцией мини ⊓, образующая решётку, и операция мини измерима по обоим аргументам. Тогда для любых функций f,g : α → M, являющихся измеримыми, функция a ↦ f(a) ⊓ g(a) измерима.
LaTeX
$$$\text{If } f,g:\alpha\to M \text{ are measurable, then } a\mapsto f(a)\sqcap g(a) \text{ is measurable.}$$$
Lean4
@[measurability]
theorem inf (hf : Measurable f) (hg : Measurable g) : Measurable fun a => f a ⊓ g a :=
measurable_inf.comp (hf.prodMk hg)
