sqrt_inv

Mathlib.Data.Real.Sqrt

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

English

For all x > 0, √(x^{-1}) = (√x)^{-1}.

Русский

Для всех x > 0: √(x^{-1}) = (√x)^{-1}.

LaTeX

$$$x > 0 \Rightarrow \sqrt{x^{-1}} = (\sqrt{x})^{-1}$$$

Lean4

@[simp]
theorem sqrt_inv (x : ℝ) : √x⁻¹ = (√x)⁻¹ := by
  rw [Real.sqrt, Real.toNNReal_inv, NNReal.sqrt_inv, NNReal.coe_inv, Real.sqrt]

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

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

Разделы

Аффилиация

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