ratLt'

Mathlib.Data.Real.Embedding

URI: https://scilib.ai/kg/mathlib#Archimedean.ratLt'

English

Equality expressing ratLt' as the image of ratLt under the Real cast map.

Русский

Эквивалентность, выражающая ratLt' как образ ratLt под отображением приведения к Real.

LaTeX

$$$\\text{ratLt'}(x) = \\operatorname{image}(\\mathrm{Rat.castHom}(\\mathbb{R})) (\\text{ratLt}(x)).$$$

Lean4

/-- `ratLt` as a set of real numbers. -/
abbrev ratLt' (x : M) : Set ℝ :=
  (Rat.castHom ℝ) '' (ratLt x)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru