inv_sub_inv_eq_inv' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- assumes `q ≠ 0` instead of `r ≠ 0`. -/
theorem inv_sub_inv_eq_inv' (hq : q ≠ 0) : r⁻¹ - q⁻¹ = p⁻¹ :=
  by
  obtain (rfl | hr) := eq_zero_or_pos r
  · suffices p = 0 by simpa [this]
    by_contra! hp
    have :=
      calc
        0⁻¹ = p⁻¹ + q⁻¹ := inv_eq p q 0
        _ < ⊤ + ⊤ := by simp [hp, hq, pos_iff_ne_zero]
        _ = ⊤ := by simp
    simp_all
  · exact inv_sub_inv_eq_inv p q hr.ne'

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