sub_one_ne_zero

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#NNReal.HolderConjugate.sub_one_ne_zero

English

If p and q are Holder conjugates in NNReal, then p − 1 ≠ 0. In particular, p > 1.

Русский

Пусть p и q — неотрицательные числа, удовлетворяющие условию сопряжённости Холдера. Тогда p > 1, следовательно p − 1 ≠ 0.

LaTeX

$$$p - 1 \\neq 0$$$

Lean4

theorem sub_one_ne_zero : p - 1 ≠ 0 :=
  h.sub_one_pos.ne'

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

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

Разделы

Аффилиация

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