rpow_left_inj

Mathlib.Analysis.SpecialFunctions.Pow.Real

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

English

If x, y ≥ 0 and z ≠ 0, then x^z = y^z iff x = y.

Русский

Если x, y ≥ 0 и z ≠ 0, то x^z = y^z эквивалентно x = y.

LaTeX

$$$x \ge 0 \land y \ge 0 \land z \neq 0 \Rightarrow x^{z} = y^{z} \iff x = y$$$

Lean4

theorem rpow_left_inj (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : z ≠ 0) : x ^ z = y ^ z ↔ x = y :=
  (rpow_left_injOn hz).eq_iff hx hy

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

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

Разделы

Аффилиация

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