comap_not — Mathlib

English

For any predicate p on α, the pullback σ-algebra along the function a ↦ ¬p a is equal to the pullback along p.

Русский

Для произвольного предиката p на α пересечение σ-алгебры, получаемой через отображение a ↦ ¬p(a), равно пересечению через p; то есть comap(¬p) = comap(p).

LaTeX

$$$\operatorname{comap}(\lambda a. \lnot p(a)) = \operatorname{comap}(p).$$$

Lean4

@[simp]
theorem comap_not (p : α → Prop) :
    MeasurableSpace.comap (fun a ↦ ¬p a) inferInstance = MeasurableSpace.comap p inferInstance :=
  MeasurableSpace.comap_compl (fun _ _ ↦ measurableSet_top) _

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