exists_measurable_proj — Mathlib

English

If s ⊆ α is measurable and nonempty, there exists a measurable map f: α → s such that f(x) = x for all x in s.

Русский

Если s ⊆ α измеримо и непусто, существует измеримая функция f: α → s такая, что f(x) = x при любом x ∈ s.

LaTeX

$$$$ \exists f: \alpha \to s,\; \text{Measurable } f \land \forall x: s, f(x)=x. $$$$

Lean4

theorem exists_measurable_proj {_ : MeasurableSpace α} (hs : MeasurableSet s) (hne : s.Nonempty) :
    ∃ f : α → s, Measurable f ∧ ∀ x : s, f x = x :=
  let ⟨f, hfm, hf⟩ :=
    (MeasurableEmbedding.subtype_coe hs).exists_measurable_extend measurable_id fun _ => hne.to_subtype
  ⟨f, hfm, congr_fun hf⟩

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