lt

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#NNReal.HolderTriple.lt

English

From HolderTriple, r < p.

Русский

Из тройки Холдера следует, что r < p.

LaTeX

$$$r < p$$$

Lean4

theorem lt : r < p :=
  h.coe.lt

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

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

Разделы

Аффилиация

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