coe_inv — Mathlib

English

The evaluation of the inverse CauSeq equals the pointwise inverse of the original sequence values.

Русский

Значение инверсной Каусевской последовательности равно покоординатно обратному значению исходной последовательности.

LaTeX

$$$ (inv\,f\,hf).\text{val}(n) = f(n)^{-1} $$$

Lean4

@[simp, norm_cast]
theorem coe_inv {f : CauSeq β abv} (hf) : ⇑(inv f hf) = (f : ℕ → β)⁻¹ :=
  rfl

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