inducedMap — Mathlib

English

The map induced by embedding α into β via rationals is defined by taking x to the supremum of the cut-map images below x.

Русский

Отображение, индуцируемое вложением из поля α в β, задаётся как верхняя граница множества rationals меньше x через cutMap.

LaTeX

$$$\\mathrm{inducedMap}(x) = \\mathrm{sSup} (\\mathrm{cutMap}\\,\\beta\\ x)$$$

Lean4

/-- The induced order-preserving function from a linear ordered field to a conditionally complete
linear ordered field, defined by taking the Sup in the codomain of all the rationals less than the
input. -/
def inducedMap (x : α) : β :=
  sSup <| cutMap β x

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