instInfSet

Mathlib.Data.Real.Archimedean

URI: https://scilib.ai/kg/mathlib#Real.instInfSet

English

The real numbers carry an infimum operation defined by inf s = - sup(-s).

Русский

У вещественных чисел существует инфиминум, равный минусу надмножество, то есть inf s = - sup(-s).

LaTeX

$$$\inf s = -\sup(-s)$$$

Lean4

noncomputable instance : InfSet ℝ :=
  ⟨fun s => -sSup (-s)⟩

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

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

Разделы

Аффилиация

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