injective_of_iterate_injective

Mathlib.Algebra.Module.LinearMap.End

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem injective_of_iterate_injective {n : ℕ} (hn : n ≠ 0) (h : Injective (f' ^ n)) : Injective f' :=
  by
  rw [← Nat.succ_pred_eq_of_pos (show 0 < n by cutsat), iterate_succ, coe_comp] at h
  exact h.of_comp

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

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

Разделы

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

Аффилиация

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