measurableSet_inl_image — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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