measurable_invFun — Mathlib

English

There is a measurable inverse function hf.invFun for a measurable embedding, and it is measurable provided Nonempty α.

Русский

У измеримого вложения существует измеримо обратное hf.invFun; измеримость гарантируется при условии, что пространство непусто.

LaTeX

$$$\\text{Measurable}(hf.invFun)$$$

Lean4

@[fun_prop, measurability]
theorem measurable_invFun [Nonempty α] (hf : MeasurableEmbedding f) : Measurable (hf.invFun : β → α) :=
  open Classical in Measurable.dite (by fun_prop) measurable_const hf.measurableSet_range

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