measurableSet_inr_image — Mathlib

English

For any set s ⊆ β, the right-injection image Sum.inr '' s is measurable in α ⊕ β if and only if s is measurable in β.

Русский

Для множества s ⊆ β образ справа Sum.inr '' s измерим в α ⊕ β тогда, когда s измеримо в β.

LaTeX

$$$\mathrm{MeasurableSet}(\mathrm{Sum.inr} '' s) \iff \mathrm{MeasurableSet}(s)$$$

Lean4

@[simp]
theorem measurableSet_inr_image {s : Set β} : MeasurableSet (Sum.inr '' s : Set (α ⊕ β)) ↔ MeasurableSet s := by
  simp [measurableSet_sum_iff, Sum.inr_injective.preimage_image]

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