embedReal — Mathlib

English

For any a in M, embedReal a equals embedRealFun a.

Русский

Для любого a ∈ M справедливо embedReal(a) = embedRealFun(a).

LaTeX

$$$\forall a\in M, \; \operatorname{embedReal}(M)(a) = \operatorname{embedRealFun}(a)$$$

Lean4

/-- The bundled `M →+o ℝ` for archimedean `M` that preserves `1`. -/
noncomputable def embedReal : M →+o ℝ where
  toFun := embedRealFun
  map_zero' := embedRealFun_zero M
  map_add' := embedRealFun_add
  monotone' := (embedRealFun_strictMono M).monotone

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