Theorems · Theorem · dynamical systems
Function.bijOn_ptsOfPeriod
∀ {α : Type u_1} (f : α → α) {n : ℕ}, 0 < n → Set.BijOn f (Function.ptsOfPeriod f n) (Function.ptsOfPeriod f n)- Defined in
- Mathlib.Dynamics.PeriodicPts.Defs
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.iterateproof · cited by 740
- Set.BijOnstatement · cited by 168
- Function.IsFixedPt.eqproof · cited by 14
- Function.ptsOfPeriodstatement and proof · cited by 6
- Function.Commute.reflproof · cited by 5
- Function.IsPeriodicPt.apply_iterateproof · cited by 4
- Function.IsPeriodicPt.eq_of_apply_eq_sameproof · cited by 2
- Function.Semiconj.mapsTo_ptsOfPeriodproof · cited by 1
- Function.comp_iterate_pred_of_posproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Function.bijOn_periodicPtsproof · cited by 0