coe_inv

Mathlib.Data.EReal.Inv

URI: https://scilib.ai/kg/mathlib#EReal.coe_inv

English

The real-to-EReal embedding commutes with inversion: for all real x, x^{-1} equals the inverse of its EReal image.

Русский

Встраивание из ℝ в EReal сохраняет операцию взятия обратного: для всех x ∈ ℝ, x^{-1} = (x)^{-1} в EReal.

LaTeX

$$$ (\uparrow x)^{-1} = \uparrow (x^{-1}) \quad (x \in \mathbb{R}) $$$

Lean4

theorem coe_inv (x : ℝ) : (x⁻¹ : ℝ) = (x : EReal)⁻¹ :=
  rfl

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

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

Разделы

Аффилиация

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