measurableSet_copy — Mathlib

English

For the copied space, a set s is measurable in the copy iff p s holds.

Русский

В копии пространства множество s измеримо тогда и только тогда, когда p s выполняется.

LaTeX

$$$\mathrm{MeasurableSet}[.\mathrm{copy}\ m\ p\ h] s \iff p s$$$

Lean4

theorem measurableSet_copy {m : MeasurableSpace α} {p : Set α → Prop} (h : ∀ s, p s ↔ MeasurableSet[m] s) {s} :
    MeasurableSet[.copy m p h] s ↔ p s :=
  Iff.rfl

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