surjective_of_iterate_surjective — Mathlib

English

If n ≠ 0 and f'^n is surjective, then f' is surjective.

Русский

Если n ≠ 0 и f'^n сюръективен, то f' сюръективен.

LaTeX

$$$n \\neq 0 \\Rightarrow (\\text{Surjective}(f'^n) \\Rightarrow \\text{Surjective}(f')).$$$

Lean4

theorem surjective_of_iterate_surjective {n : ℕ} (hn : n ≠ 0) (h : Surjective (f' ^ n)) : Surjective f' :=
  by
  rw [← Nat.succ_pred_eq_of_pos (Nat.pos_iff_ne_zero.mpr hn), pow_succ', coe_mul] at h
  exact Surjective.of_comp h

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