inv_two_add_inv_two

Mathlib.Data.ENNReal.Inv

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

English

In ENNReal, (2)^{-1} + 2^{-1} = 1.

Русский

В ENNReal выполняется 2^{-1} + 2^{-1} = 1.

LaTeX

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

Lean4

theorem inv_two_add_inv_two : (2 : ℝ≥0∞)⁻¹ + 2⁻¹ = 1 := by
  rw [← two_mul, ← div_eq_mul_inv, ENNReal.div_self two_ne_zero ofNat_ne_top]

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

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

Разделы

Аффилиация

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