holderConjugate_coe_iff — Mathlib

English

HolderConjugate on ENNReal coincides with NNRealHolderConjugate after coercion.

Русский

Сопряжённость Холдера для ENNReal совпадает с таковой для NNReal после вложения.

LaTeX

$$HolderConjugate (p : ℝ≥0∞) (q : ℝ≥0∞) ↔ NNReal.HolderConjugate p q$$

Lean4

@[simp, norm_cast]
theorem holderConjugate_coe_iff {p q : ℝ≥0} : HolderConjugate (p : ℝ≥0∞) (q : ℝ≥0∞) ↔ NNReal.HolderConjugate p q :=
  holderTriple_coe_iff one_ne_zero

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