Theorems · Theorem · dynamical systems
CircleDeg1Lift.tendsto_translationNumber_aux
∀ (f : CircleDeg1Lift), Filter.Tendsto f.transnumAuxSeq Filter.atTop (nhds f.translationNumber)
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- nhdsstatement · cited by 5,554
- Filter.Tendstostatement · cited by 3,814
- Filter.atTopstatement · cited by 2,405
- le_of_ltproof · cited by 1,175
- CircleDeg1Liftstatement and proof · cited by 128
- CircleDeg1Lift.translationNumberstatement · cited by 48
- CircleDeg1Lift.transnumAuxSeqstatement · cited by 6
- CauchySeq.tendsto_limUnderproof · cited by 3
- CircleDeg1Lift.transnumAuxSeq_dist_ltproof · cited by 2
- cauchySeq_of_le_geometric_twoproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- CircleDeg1Lift.tendsto_translationNumber_of_dist_bounded_auxproof · cited by 2
- CircleDeg1Lift.translationNumber_mul_of_commuteproof · cited by 1
- CircleDeg1Lift.dist_map_zero_translationNumber_leproof · cited by 1