pos'

Mathlib.Data.Real.ConjExponents

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

English

From the Holder triple, the third exponent r is positive: r > 0.

Русский

Из условия тройки Холдера следует, что третий показатель r положителен: r > 0.

LaTeX

$$$0 < r$$$

Lean4

/-- For `r`, instead of `p` -/
theorem pos' : 0 < r :=
  inv_pos.mp <| h.inv_add_inv_eq_inv ▸ add_pos h.inv_pos h.symm.inv_pos

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

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

Разделы

Аффилиация

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