inv_one_sub_inv

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#ENNReal.HolderConjugate.inv_one_sub_inv

English

If h : NNReal.HolderConjugate p.toNNReal q.toNNReal, then p.HolderConjugate q.

Русский

Если h : NNReal.HolderConjugate p.toNNReal q.toNNReal, то p.HolderConjugate q.

LaTeX

$$$NNReal.HolderConjugate(p.toNNReal, q.toNNReal) \\Rightarrow HolderConjugate(p, q)$$$

Lean4

theorem inv_one_sub_inv (ha : a ≤ 1) : a⁻¹.HolderConjugate (1 - a)⁻¹ :=
  .inv_inv <| add_tsub_cancel_of_le ha

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

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

Разделы

Аффилиация

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