Theorems · Theorem · dynamical systems
Function.bijOn_periodicPts
∀ {α : Type u_1} (f : α → α), Set.BijOn f (Function.periodicPts f) (Function.periodicPts f)- Defined in
- Mathlib.Dynamics.PeriodicPts.Lemmas
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PNatproof · cited by 392
- Set.BijOnstatement · cited by 168
- Function.periodicPtsstatement · cited by 33
- PNat.posproof · cited by 9
- Function.bijOn_ptsOfPeriodproof · cited by 1
- Set.bijOn_iUnion_of_directedproof · cited by 1
- Function.iUnion_pnat_ptsOfPeriodproof · cited by 1
- Function.directed_ptsOfPeriod_pnatproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.