inverse_one_sub — Mathlib

English

For t with ‖t‖ < 1, the inverse of 1 − t equals the inverse of the unit oneSub t h (i.e., (1 − t)⁻¹ = (oneSub t h)⁻¹).

Русский

Для t с ‖t‖ < 1 обратное к 1 − t равно обратному единице oneSub t h (то есть (1 − t)⁻¹ = (oneSub t h)⁻¹).

LaTeX

$$$\|t\|<1 \Rightarrow (1-t)^{-1} = (\text{Units.oneSub } t h)^{-1}.$$$

Lean4

theorem inverse_one_sub (t : R) (h : ‖t‖ < 1) : inverse (1 - t) = ↑(Units.oneSub t h)⁻¹ := by
  rw [← inverse_unit (Units.oneSub t h), Units.val_oneSub]

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