measurableSub — Mathlib

English

If γ is equipped with a continuous subtraction, then the maps a ↦ c − a and a ↦ a − c (for fixed c) are measurable.

Русский

Если в γ задано непрерывное вычитание, то отображения a ↦ c − a и a ↦ a − c (для фиксированного c) измеримы.

LaTeX

$$$\\forall c:\\gamma,\\mathrm{Measurable}(\\lambda a:\\gamma, c-a)\\ \\land\\ \\mathrm{Measurable}(\\lambda a:\\gamma, a-c)$$$

Lean4

instance (priority := 100) measurableSub [Sub γ] [ContinuousSub γ] : MeasurableSub γ
    where
  measurable_const_sub _ := (continuous_const.sub continuous_id).measurable
  measurable_sub_const _ := (continuous_id.sub continuous_const).measurable

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