one_sub_inv_two

Mathlib.Data.ENNReal.Inv

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

English

1 − 2^{-1} = 2^{-1} in ENNReal.

Русский

1 − 2^{-1} = 2^{-1} в ENNReal.

LaTeX

$$$$ 1 - 2^{-1} = 2^{-1}. $$$$

Lean4

@[simp]
theorem one_sub_inv_two : (1 : ℝ≥0∞) - 2⁻¹ = 2⁻¹ := by rw [← one_div, sub_half one_ne_top]

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

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

Разделы

Аффилиация

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