instConditionallyCompleteLinearOrderedFieldReal

Mathlib.Data.Real.CompleteField

URI: https://scilib.ai/kg/mathlib#instConditionallyCompleteLinearOrderedFieldReal

English

The real numbers form a ConditionallyCompleteLinearOrderedField.

Русский

Действительные числа образуют условно полно упорядченное линейно упорядованное поле.

LaTeX

$$$\mathrm{CCLOF}(\mathbb{R})$$$

Lean4

/-- The reals are a conditionally complete linearly ordered field. -/
noncomputable instance : ConditionallyCompleteLinearOrderedField ℝ :=
  { }

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

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

Разделы

Аффилиация

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