measurableSet_comap — Mathlib

English

The comapped measurable space equals the generateFrom of the sets characterized by preimages under f.

Русский

Обозначение comap равно generateFrom множества, задаваемого пообратному образу под f.

LaTeX

$$$m.comap f = \text{generateFrom} \{t \mid \exists s, \text{MeasurableSet}(s) \wedge f^{-1}(s) = t\}$$$

Lean4

theorem measurableSet_comap {m : MeasurableSpace β} :
    MeasurableSet[m.comap f] s ↔ ∃ s', MeasurableSet[m] s' ∧ f ⁻¹' s' = s :=
  .rfl

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