one_half_lt_one

Mathlib.Data.ENNReal.Inv

URI: https://scilib.ai/kg/mathlib#ENNReal.one_half_lt_one

English

The reciprocal of 2 is less than 1 in ENNReal: (2)^{-1} < 1.

Русский

Обратное к 2 меньше 1 в ENNReal: 2^{-1} < 1.

LaTeX

$$$$ (2)^{-1} < 1. $$$$

Lean4

protected theorem one_half_lt_one : (2⁻¹ : ℝ≥0∞) < 1 :=
  ENNReal.inv_lt_one.2 <| one_lt_two

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

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

Разделы

Аффилиация

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