toMeasurableDiv₂ — Mathlib

English

If α has a discrete measurable structure, then the operation (β) → α×α → α with two-argument division is measurable.

Русский

Если у α дискретная сигма-алгебра, то двоичная операция деления измерима.

LaTeX

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

Lean4

@[to_additive DiscreteMeasurableSpace.toMeasurableSub₂] -- See note [lower instance priority]

instance (priority := 100) toMeasurableDiv₂ [DiscreteMeasurableSpace (α × α)] : MeasurableDiv₂ α :=
  ⟨.of_discrete⟩

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