to_hasMeasurableInf — Mathlib

English

There exists a MeasurableInf structure on M, given by the meet ⊓, such that the map (x,y) ↦ x ⊓ y is measurable in each argument.

Русский

Существует структуру измеримого инфа на M, заданную через операцию ⊓, где функция (x,y) ↦ x ⊓ y измерима по каждому аргументу.

LaTeX

$$$\text{MeasurableInf } M\text{ holds, i.e., the binary operation }\inf\text{ is measurable in each argument.}$$$

Lean4

instance (priority := 100) to_hasMeasurableInf : MeasurableInf M :=
  ⟨fun _ => measurable_const.inf measurable_id, fun _ => measurable_id.inf measurable_const⟩

Похожие утверждения