ofPowerSeries_injective — Mathlib

English

The inverse of toPowerSeries is injective, hence the inverse of ofPowerSeries is injective as well.

Русский

Обратно к toPowerSeries инъективно, следовательно и обратное отображение ofPowerSeries инъективно.

LaTeX

$$$ \text{ofPowerSeries}^{-1} \text{ injective} $$$

Lean4

theorem ofPowerSeries_injective : Function.Injective (ofPowerSeries Γ R) :=
  embDomain_injective.comp toPowerSeries.symm.injective

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