comap_compl — Mathlib

English

The comap of the complement operation along a measurable function equals the comap of the function itself (Boolean algebra setting).

Русский

Comap операции дополнения вдоль измеримой функции равен comap самой функции (в контексте буловой алгебры).

LaTeX

$$$\\mathrm{MeasurableSpace.comap}\\ \\big(\\lambda a. (f(a))^{\\complement}\\big) = \\mathrm{MeasurableSpace.comap} f$$$

Lean4

theorem comap_compl {m' : MeasurableSpace β} [BooleanAlgebra β] (h : Measurable (compl : β → β)) (f : α → β) :
    MeasurableSpace.comap (fun a => (f a)ᶜ) inferInstance = MeasurableSpace.comap f inferInstance :=
  by
  rw [← Function.comp_def, ← MeasurableSpace.comap_comp]
  congr
  exact (MeasurableEquiv.ofInvolutive _ compl_involutive h).measurableEmbedding.comap_eq

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