fact_zero_lt_one

Mathlib.Data.Real.Basic

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

English

As a fact, 0 < 1 holds in the real numbers.

Русский

Как факт, 0 < 1 верно для вещественных чисел.

LaTeX

$$$0 < 1$$$

Lean4

@[deprecated ZeroLEOneClass.factZeroLtOne (since := "2025-05-12")]
protected theorem fact_zero_lt_one : Fact ((0 : ℝ) < 1) :=
  ⟨Real.zero_lt_one⟩

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

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

Разделы

Аффилиация

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