map_derivedSeries_eq — Mathlib

English

If f is surjective, then the image of the nth derived series equals the nth derived series of the codomain: (derivedSeries G n).map f = derivedSeries G' n.

Русский

Если f сюръективен, то образ n-й производящей серии совпадает с n-й производящей серией G': (derivedSeries G n).map f = derivedSeries G' n.

LaTeX

$$(derivedSeries(G,n)).map f = derivedSeries(G',n)$$

Lean4

theorem map_derivedSeries_eq (hf : Function.Surjective f) (n : ℕ) : (derivedSeries G n).map f = derivedSeries G' n :=
  le_antisymm (map_derivedSeries_le_derivedSeries f n) (derivedSeries_le_map_derivedSeries hf n)

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