holderTriple_coe_iff — Mathlib

English

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

Русский

Для p,q,r ∈ ℝ≥0 истинно Real.HolderTriple(p, q, r) тогда, когда HolderTriple p q r истинно.

LaTeX

$$$Real.HolderTriple(p : \mathbb{R}) (q : \mathbb{R}) (r : \mathbb{R}) \iff HolderTriple p q r \quad \text{при } p,q,r \ge 0$$$

Lean4

@[simp, norm_cast]
theorem holderTriple_coe_iff {p q r : ℝ≥0} : Real.HolderTriple (p : ℝ) (q : ℝ) (r : ℝ) ↔ HolderTriple p q r := by
  rw_mod_cast [Real.holderTriple_iff, holderTriple_iff]

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