map_surjective — Mathlib

English

If f is surjective, the induced map on power series is surjective.

Русский

Если f сюръективен, то отображение степенных рядов на него сюръективно.

LaTeX

$$$\mathrm{Surjective}(\mathrm{PowerSeries.map}\, f)$$$

Lean4

theorem map_surjective (f : S →+* T) (hf : Function.Surjective f) : Function.Surjective (PowerSeries.map f) :=
  by
  intro g
  use PowerSeries.mk fun k ↦ Function.surjInv hf (PowerSeries.coeff k g)
  ext k
  simp only [Function.surjInv, coeff_map, coeff_mk]
  exact Classical.choose_spec (hf (coeff k g))

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