subtype_mk — Mathlib

English

If f : α → β is measurable, then the range factorization of f is measurable.

Русский

Если f : α → β измеримо, тогда факторизация диапазона f измерима.

LaTeX

$$$\\\\operatorname{Measurable}(\\\\text{rangeFactorization}(f))$$$

Lean4

@[measurability]
theorem subtype_mk {p : β → Prop} {f : α → β} (hf : Measurable f) {h : ∀ x, p (f x)} :
    Measurable fun x => (⟨f x, h x⟩ : Subtype p) := fun t ⟨s, hs⟩ =>
  hs.2 ▸ by simp only [← preimage_comp, Function.comp_def, hf hs.1]

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