inv_sub_inv_eq_inv — Mathlib

English

If p, q, r ∈ ENNReal satisfy HolderTriple p q r and r ≠ 0, then r⁻¹ − q⁻¹ = p⁻¹.

Русский

Пусть p, q, r ∈ ENNReal удовлетворяют HolderTriple p q r и r ≠ 0. Тогда r⁻¹ − q⁻¹ = p⁻¹.

LaTeX

$$$HolderTriple(p,q,r) \land r \neq 0 \Rightarrow r^{-1} - q^{-1} = p^{-1}$$$

Lean4

theorem inv_sub_inv_eq_inv (hr : r ≠ 0) : r⁻¹ - q⁻¹ = p⁻¹ :=
  by
  apply ENNReal.sub_eq_of_eq_add (ne_of_lt ?_) (inv_eq p q r)
  calc
    q⁻¹ ≤ r⁻¹ := HolderTriple.inv_le_inv q p r
    _ < ∞ := by simpa using pos_iff_ne_zero.mpr hr

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