toMeasurableDiv — Mathlib

English

In a discrete measurable space, the division by a fixed element is measurable.

Русский

В дискретном измеримом пространстве деление на фиксированный элемент измеримо.

LaTeX

$$$\text{MeasurableDiv}\,\alpha$$$

Lean4

@[to_additive] -- See note [lower instance priority]

instance (priority := 100) toMeasurableDiv [DiscreteMeasurableSpace α] : MeasurableDiv α
    where
  measurable_const_div _ := .of_discrete
  measurable_div_const _ := .of_discrete

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