rpow_one_sub'

Mathlib.Analysis.SpecialFunctions.Pow.Real

URI: https://scilib.ai/kg/mathlib#Real.rpow_one_sub'

English

Let x > 0 and 1 - y ≠ 0. Then x^{1 - y} = x / x^y.

Русский

Пусть x > 0 и 1 - y ≠ 0. Тогда x^{1 - y} = x / x^y.

LaTeX

$$$\\\\forall x > 0, \\\\forall y \\\\in \\\\mathbb{R}, \ (1 - y) \neq 0 \Rightarrow x^{\, 1 - y} = \\frac{x}{x^y}.$$$

Lean4

theorem rpow_one_sub' (hx : 0 ≤ x) (h : 1 - y ≠ 0) : x ^ (1 - y) = x / x ^ y := by rw [rpow_sub' hx h, rpow_one]

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

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

Разделы

Аффилиация

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