rpow_two

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#NNReal.rpow_two

English

For x ≥ 0, x^2 (as real power) equals x^2 (as natural power).

Русский

Для x ≥ 0 выражение x^2 через действительную степень равно x^2 через целую степень.

LaTeX

$$x \ge 0 \Rightarrow x^{2} = x^{2}$$

Lean4

theorem rpow_two (x : ℝ≥0) : x ^ (2 : ℝ) = x ^ 2 :=
  rpow_ofNat x 2

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

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

Разделы

Аффилиация

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