unique_of_ne_zero — Mathlib

English

Let p, q, r ∈ ENNReal satisfy HolderTriple p q r with r ≠ 0. If q' satisfies HolderTriple p q' r, then q = q'.

Русский

Пусть p, q, r ∈ ENNReal удовлетворяют HolderTriple p q r и r ≠ 0. Если q' удовлетворяет HolderTriple p q' r, то q = q'.

LaTeX

$$$HolderTriple(p,q,r) \land r \neq 0 \Rightarrow (\forall q' , HolderTriple(p,q',r) \Rightarrow q = q')$$$

Lean4

theorem unique_of_ne_zero (q' : ℝ≥0∞) (hr : r ≠ 0) [HolderTriple p q' r] : q = q' := by
  rw [← inv_inj, ← inv_sub_inv_eq_inv q p hr, ← inv_sub_inv_eq_inv q' p hr]

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