comap_eq_generateFrom — Mathlib

English

The comap of a measurable space by f equals the generateFrom of preimage-sets.

Русский

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

LaTeX

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

Lean4

theorem comap_eq_generateFrom (m : MeasurableSpace β) (f : α → β) :
    m.comap f = generateFrom {t | ∃ s, MeasurableSet s ∧ f ⁻¹' s = t} :=
  (@generateFrom_measurableSet _ (.comap f m)).symm

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