cutMap — Mathlib

English

The cut map coincides with a cut defined by an interval and rationals: cutMap α a = Iio(a) ∩ image(Rat.cast).

Русский

Разрезная карта совпадает с разрезом, заданным интервалом и рациональными числами: cutMap α a = Iio(a) ∩ образ Rat.cast.

LaTeX

$$$\operatorname{cutMap}_{\alpha}(a) = Iio(a) \cap \operatorname{range}(\operatorname{Rat.cast} : \mathbb{Q} \to \alpha)$$$

Lean4

/-- The lower cut of rationals inside a linear ordered field that are less than a given element of
another linear ordered field. -/
def cutMap (a : α) : Set β :=
  (Rat.cast : ℚ → β) '' {t | ↑t < a}

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