subtype_coe — Mathlib

English

If f : α → β is measurable, then the function a ↦ (f a) (viewed as an element of β) is measurable.

Русский

Если f : α → β измеримо, то функция a ↦ (f a) с точностью до типа Subtype p измерима.

LaTeX

$$$\\\\operatorname{Measurable}((\\\\uparrow) : \\\\mathrm{Subtype}(p) \\\\rightarrow \\\\alpha) \\\\Rightarrow \\\\operatorname{Measurable}(\\\\lambda a \\\\:\\\\rightarrow (f a))$$$

Lean4

@[measurability]
theorem subtype_coe {p : β → Prop} {f : α → Subtype p} (hf : Measurable f) : Measurable fun a : α => (f a : β) :=
  measurable_subtype_coe.comp hf

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