holderConjugate_coe_iff

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#NNReal.holderConjugate_coe_iff

← MathLib Explorer

English

For p,q ∈ ℝ≥0, Real.HolderConjugate (p) (q) holds iff HolderConjugate p q.

Русский

Для p,q ∈ ℝ≥0 Real.HolderConjugate (p) (q) эквивалентно HolderConjugate p q.

LaTeX

$$$(Real.HolderConjugate (p : \mathbb{R}) (q : \mathbb{R})) \iff (HolderConjugate p q)$$$

Lean4

@[simp, norm_cast]
theorem holderConjugate_coe_iff {p q : ℝ≥0} : Real.HolderConjugate (p : ℝ) (q : ℝ) ↔ HolderConjugate p q :=
  holderTriple_coe_iff (r := 1)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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