_aux_Mathlib_MeasureTheory_Function_StronglyMeasurable_Basic___macroRules_MeasureTheory_termStronglyMeasurable[_]_1

English

A constant function is strongly measurable.

Русский

Постоянная функция является сильно-измеримой.

LaTeX

$$$\\text{StronglyMeasurable}( \\text{const } b )$$$

Lean4

@[scoped macro MeasureTheory.«termStronglyMeasurable[_]»]
public meta def
  «_aux_Mathlib_MeasureTheory_Function_StronglyMeasurable_Basic___macroRules_MeasureTheory_termStronglyMeasurable[_]_1» :
    Macro✝ := fun
  | `(StronglyMeasurable[$m]) => ``(@MeasureTheory.StronglyMeasurable _ _ _ $m)
  | _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝

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