subtype_image — Mathlib

English

If s and t are measurable, then the image of t under the Subtype.val map is measurable in α.

Русский

Если s и t — измеримые, то образ t через Subtype.val в α измерим.

LaTeX

$$$\\\\operatorname{MeasurableSet}(s) \\\\wedge \\\\operatorname{MeasurableSet}(t) \\\\Rightarrow \\\\operatorname{MeasurableSet}(\\\\operatorname{image}(\\\\operatorname{Subtype}.val, t))$$$

Lean4

theorem subtype_image {s : Set α} {t : Set s} (hs : MeasurableSet s) :
    MeasurableSet t → MeasurableSet (((↑) : s → α) '' t) :=
  by
  rintro ⟨u, hu, rfl⟩
  rw [Subtype.image_preimage_coe]
  exact hs.inter hu

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