inv_add_inv_ennreal — Mathlib

English

If p and q are real Holder conjugates, then (ENNReal.ofReal p)^{-1} + (ENNReal.ofReal q)^{-1} = 1.

Русский

Если p и q сопряжены Холдером, то (ENNReal.ofReal p)^{-1} + (ENNReal.ofReal q)^{-1} = 1.

LaTeX

$$$(ENNReal.ofReal\ p)^{-1} + (ENNReal.ofReal\ q)^{-1} = 1$$

Lean4

theorem inv_add_inv_ennreal : (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1 := by
  rw [← ENNReal.ofReal_one, ← ENNReal.ofReal_inv_of_pos h.pos, ← ENNReal.ofReal_inv_of_pos h.symm.pos, ←
    ENNReal.ofReal_add h.inv_nonneg h.symm.inv_nonneg, h.inv_add_inv_eq_one]

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