image_of_antitoneOn — Mathlib

English

The image of a measurable set under an antitone map is measurable.

Русский

Образ измеримого множества под антитонной картой измерим.

LaTeX

$$MeasurableSet (g '' t)$$

Lean4

/-- The image of a measurable set under an antitone map is measurable. -/
theorem image_of_antitoneOn [SecondCountableTopology β] (ht : MeasurableSet t) (hg : AntitoneOn g t) :
    MeasurableSet (g '' t) :=
  (ht.image_of_monotoneOn hg.dual_right :)

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