iterate_surjective

Mathlib.Algebra.Module.LinearMap.End

URI: https://scilib.ai/kg/mathlib#Module.End.iterate_surjective

← MathLib Explorer

English

If f' is surjective, then for every n, f'^n is surjective.

Русский

Если f' сюръективен, то для каждого n сюръективно f'^n.

LaTeX

$$$\\forall n,\\; \\text{Surjective}(f'^n).$$$

Lean4

theorem iterate_surjective (h : Surjective f') : ∀ n : ℕ, Surjective (f' ^ n)
  | 0 => surjective_id
  | n + 1 => by
    rw [iterate_succ]
    exact (iterate_surjective h n).comp h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru