embeddingReal — Mathlib

English

The object embeddingReal is a function from a type to the real numbers, intended as a canonical real-valued embedding.

Русский

Объект embeddingReal есть функция из типа в множество вещественных чисел, каноническое встраивание.

LaTeX

$$$\text{embeddingReal} : \Omega \to \mathbb{R}$.$$

Lean4

/-- A measurable embedding of a standard Borel space into `ℝ`. -/
noncomputable def embeddingReal (Ω : Type*) [MeasurableSpace Ω] [StandardBorelSpace Ω] : Ω → ℝ :=
  (exists_measurableEmbedding_real Ω).choose

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