sInf_univ

Mathlib.Data.Real.Archimedean

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

English

The infimum of the universal set is 0.

Русский

Infimum множества ℝ равно 0.

LaTeX

$$$sInf(\mathrm{Set.univ}) = 0$$$

Lean4

theorem sInf_univ : sInf (@Set.univ ℝ) = 0 := by simp [sInf_def]

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

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

Разделы

Аффилиация

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