Theorems · Theorem · dynamical systems
Function.iterate_succ_apply
∀ {α : Type u} (f : α → α) (n : ℕ) (x : α), f^[n.succ] x = f^[n] (f x)- Defined in
- Mathlib.Logic.Function.Iterate
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.iteratestatement · cited by 740
Cited by18
Results whose statement or proof uses this declaration.
- Function.iterate_fixedproof · cited by 9
- iteratedDeriv_succ'proof · cited by 5
- Monotone.monotone_iterate_of_le_mapproof · cited by 3
- Polynomial.iterate_derivative_eq_zeroproof · cited by 3
- fwdDiff_iter_pow_eq_zero_of_ltproof · cited by 3
- Ordinal.iterate_lt_nfpproof · cited by 2
- Turing.TM1to1.trTape'_move_rightproof · cited by 1
- ODE.FunSpace.dist_iterate_iterate_next_le_of_lipschitzWithproof · cited by 1
- ODE.FunSpace.dist_iterate_next_leproof · cited by 1
- ContractingWith.isFixedPt_fixedPoint_iterateproof · cited by 1
- WittVector.iterate_verschiebung_mul_leftproof · cited by 1
- StrictMono.strictMono_iterate_of_lt_mapproof · cited by 1