`iterate`

definition

show as: view math explainer →

module: IndisputableMonolith.Compat.FunctionIterate
domain: Compat
line: 19 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Compat.FunctionIterate on GitHub at line 19.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

succ IndisputableMonolith.Foundation.ArithmeticFromLogic
diagonal_continuous_on_range IndisputableMonolith.Foundation.PolynomialityFromLogic
iterate_continuous_on_range IndisputableMonolith.Foundation.PolynomialityFromLogic
tickEquivLogicNat IndisputableMonolith.Foundation.TimeAsOrbit
tick_orbit_eq_logicNat_succ IndisputableMonolith.Foundation.TimeAsOrbit
cascade_doubly_exponential_lower IndisputableMonolith.NumberTheory.CompositionDivergence
ScheduleNeutralityCert IndisputableMonolith.URCGenerators.LNALCerts
lCycle IndisputableMonolith.VM.State

formal source

  16variable {α : Sort u}
  17
  18/-- Compatibility definition: iterate `f` for `n` steps starting from `a`. -/
  19def iterate (f : α → α) (n : Nat) (a : α) : α :=
  20  Nat.iterate f n a
  21
  22end Function

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.