measurableSet_plusPart — Mathlib

English

If A is measurable, then negAt s '' (plusPart A) is measurable; in particular, its image is measurable.

Русский

Если A измеримо, то negAt s '' (plusPart A) измеримо; образ также измерим.

LaTeX

$$MeasurableSet(negAt(s)''(plusPart(A)))$$

Lean4

theorem measurableSet_plusPart (hm : MeasurableSet A) : MeasurableSet (plusPart A) :=
  by
  convert_to MeasurableSet (A ∩ (⋂ w, {x | 0 < x.1 w}))
  · ext; simp
  · refine hm.inter (MeasurableSet.iInter fun _ ↦ ?_)
    exact measurableSet_lt measurable_const ((measurable_pi_apply _).comp' measurable_fst)

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