measurable_iff_comap_le — Mathlib

English

A function f is measurable iff the comap of the codomain along f is below the domain's measurable structure.

Русский

Функция f измерима тогда и только тогда, когда comap f ниже структуры измеримости домена.

LaTeX

$$$$ \text{Measurable} f \;\iff\; m_{2}.\mathrm{comap} f \le m_{1} $$$$

Lean4

theorem measurable_iff_comap_le {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β} :
    Measurable f ↔ m₂.comap f ≤ m₁ :=
  comap_le_iff_le_map.symm

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