TranslationNumber

📁 Source: Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean

Statistics

Metric	Count
Definitions CircleDeg1Lift, instFunLikeReal, instInhabited, instLattice, instMonoid, toOrderHom, toOrderIso, translate, translationNumber, transnumAuxSeq, unitsHasCoeToFun	11
Theorems ceil_map_map_zero_le, coe_mk, coe_mul, coe_one, coe_pow, coe_toOrderHom, coe_toOrderIso, coe_toOrderIso_inv, coe_toOrderIso_symm, commute_add_int, commute_add_nat, commute_iff_commute, commute_int_add, commute_nat_add, commute_sub_int, commute_sub_nat, continuous_iff_surjective, continuous_pow, dist_map_map_zero_lt, dist_map_zero_lt_of_semiconj, dist_map_zero_lt_of_semiconjBy, dist_map_zero_translationNumber_le, dist_pow_map_zero_mul_translationNumber_le, exists_eq_add_translationNumber, ext, ext_iff, floor_map_map_zero_le, floor_sub_le_translationNumber, forall_map_sub_of_Icc, inf_apply, instOrderHomClassReal, isUnit_iff_bijective, iterate_eq_of_map_eq_add_int, iterate_le_of_map_le_add_int, iterate_mono, iterate_monotone, iterate_pos_eq_iff, iterate_pos_le_iff, iterate_pos_lt_iff, le_ceil_map_map_zero, le_floor_map_map_zero, le_iterate_of_add_int_le_map, le_iterate_pos_iff, le_map_map_zero, le_map_of_map_zero, le_translationNumber_of_add_int_le, le_translationNumber_of_add_le, le_translationNumber_of_add_nat_le, lt_iterate_pos_iff, lt_map_map_zero, lt_map_of_int_lt_translationNumber, lt_map_of_nat_lt_translationNumber, lt_translationNumber_of_forall_add_lt, map_add_int, map_add_nat, map_add_one, map_add_one', map_fract_sub_fract_eq, map_int_add, map_int_of_map_zero, map_le_of_map_zero, map_lt_add_floor_translationNumber_add_one, map_lt_add_translationNumber_add_one, map_lt_of_translationNumber_lt_int, map_lt_of_translationNumber_lt_nat, map_map_zero_le, map_map_zero_lt, map_nat_add, map_one_add, map_sub_int, map_sub_nat, mono, monotone, mul_apply, mul_floor_map_zero_le_floor_iterate_zero, pow_mono, pow_monotone, semiconjBy_iff_semiconj, semiconj_of_bijective_of_translationNumber_eq, semiconj_of_group_action_of_forall_translationNumber_eq, semiconj_of_isUnit_of_translationNumber_eq, strictMono_iff_injective, sup_apply, tendsto_atBot, tendsto_atTop, tendsto_translationNumber, tendsto_translationNumber_aux, tendsto_translationNumber_of_dist_bounded_aux, tendsto_translation_number', tendsto_translation_number₀, tendsto_translation_number₀', translate_apply, translate_inv_apply, translate_iterate, translate_pow, translate_zpow, translationNumber_conj_eq, translationNumber_conj_eq', translationNumber_eq_int_iff, translationNumber_eq_of_dist_bounded, translationNumber_eq_of_semiconj, translationNumber_eq_of_semiconjBy, translationNumber_eq_of_tendsto_aux, translationNumber_eq_of_tendsto₀, translationNumber_eq_of_tendsto₀', translationNumber_eq_rat_iff, translationNumber_le_ceil_sub, translationNumber_le_of_le_add, translationNumber_le_of_le_add_int, translationNumber_le_of_le_add_nat, translationNumber_lt_of_forall_lt_add, translationNumber_mono, translationNumber_mul_of_commute, translationNumber_of_eq_add_int, translationNumber_of_map_pow_eq_add_int, translationNumber_one, translationNumber_pow, translationNumber_translate, translationNumber_units_inv, translationNumber_zpow, transnumAuxSeq_def, transnumAuxSeq_dist_lt, transnumAuxSeq_zero, units_apply_inv_apply, units_inv_apply_apply, units_semiconj_of_translationNumber_eq	126
Total	137

CircleDeg1Lift

Definitions

Name	Category	Theorems
instFunLikeReal 📖	CompOp	82 math math: mono, units_inv_apply_apply, instOrderHomClassReal, translate_inv_apply, map_sub_int, map_add_nat, commute_nat_add, iterate_pos_le_iff, iterate_pos_lt_iff, isUnit_iff_bijective, commute_iff_commute, dist_map_zero_translationNumber_le, map_lt_add_floor_translationNumber_add_one, tendsto_atBot, strictMono_iff_injective, floor_sub_le_translationNumber, map_one_add, map_le_of_map_zero, le_map_of_map_zero, ext_iff, dist_map_map_zero_lt, inf_apply, lt_map_of_nat_lt_translationNumber, coe_toOrderIso_symm, translate_iterate, map_int_of_map_zero, coe_toOrderIso_inv, units_apply_inv_apply, map_map_zero_lt, le_floor_map_map_zero, coe_mk, mul_apply, transnumAuxSeq_zero, lt_map_of_int_lt_translationNumber, iterate_mono, tendsto_translation_number', map_nat_add, commute_add_int, continuous_iff_surjective, iterate_monotone, commute_sub_int, commute_add_nat, semiconj_of_isUnit_of_translationNumber_eq, le_map_map_zero, map_sub_nat, transnumAuxSeq_def, coe_mul, translate_apply, translationNumber_le_ceil_sub, dist_pow_map_zero_mul_translationNumber_le, semiconj_of_group_action_of_forall_translationNumber_eq, coe_toOrderIso, map_add_int, le_ceil_map_map_zero, coe_one, commute_int_add, lt_iterate_pos_iff, tendsto_translation_number₀, tendsto_atTop, lt_map_map_zero, sup_apply, ceil_map_map_zero_le, map_int_add, monotone, coe_toOrderHom, units_semiconj_of_translationNumber_eq, le_iterate_pos_iff, map_lt_add_translationNumber_add_one, coe_pow, map_lt_of_translationNumber_lt_nat, tendsto_translationNumber, map_fract_sub_fract_eq, floor_map_map_zero_le, map_map_zero_le, mul_floor_map_zero_le_floor_iterate_zero, iterate_pos_eq_iff, dist_map_zero_lt_of_semiconjBy, map_add_one, commute_sub_nat, tendsto_translation_number₀', semiconjBy_iff_semiconj, map_lt_of_translationNumber_lt_int
instInhabited 📖	CompOp	—
instLattice 📖	CompOp	5 math math: inf_apply, iterate_monotone, sup_apply, pow_monotone, translationNumber_mono
instMonoid 📖	CompOp	35 math math: units_inv_apply_apply, translate_inv_apply, isUnit_iff_bijective, commute_iff_commute, pow_mono, translationNumber_eq_rat_iff, translationNumber_one, coe_toOrderIso_symm, translate_iterate, coe_toOrderIso_inv, units_apply_inv_apply, mul_apply, tendsto_translation_number', continuous_pow, transnumAuxSeq_def, coe_mul, translate_apply, dist_pow_map_zero_mul_translationNumber_le, coe_toOrderIso, translate_zpow, le_ceil_map_map_zero, coe_one, tendsto_translation_number₀, translationNumber_conj_eq, pow_monotone, coe_pow, translationNumber_conj_eq', tendsto_translationNumber, translationNumber_translate, translationNumber_units_inv, translationNumber_pow, translate_pow, tendsto_translation_number₀', translationNumber_zpow, semiconjBy_iff_semiconj
toOrderHom 📖	CompOp	2 math math: coe_toOrderHom, map_add_one'
toOrderIso 📖	CompOp	3 math math: coe_toOrderIso_symm, coe_toOrderIso_inv, coe_toOrderIso
translate 📖	CompOp	6 math math: translate_inv_apply, translate_iterate, translate_apply, translate_zpow, translationNumber_translate, translate_pow
translationNumber 📖	CompOp	40 math math: translationNumber_mul_of_commute, tendsto_translationNumber_aux, translationNumber_le_of_le_add, dist_map_zero_translationNumber_le, le_translationNumber_of_add_int_le, map_lt_add_floor_translationNumber_add_one, translationNumber_eq_rat_iff, translationNumber_eq_of_tendsto₀', translationNumber_one, floor_sub_le_translationNumber, translationNumber_eq_of_semiconj, tendsto_translation_number', translationNumber_of_map_pow_eq_add_int, translationNumber_of_eq_add_int, translationNumber_le_ceil_sub, dist_pow_map_zero_mul_translationNumber_le, translationNumber_le_of_le_add_int, translationNumber_eq_of_semiconjBy, translationNumber_eq_of_tendsto₀, tendsto_translation_number₀, translationNumber_eq_of_dist_bounded, translationNumber_le_of_le_add_nat, translationNumber_conj_eq, exists_eq_add_translationNumber, le_translationNumber_of_add_le, translationNumber_lt_of_forall_lt_add, map_lt_add_translationNumber_add_one, translationNumber_conj_eq', tendsto_translationNumber, translationNumber_translate, translationNumber_units_inv, translationNumber_eq_of_tendsto_aux, translationNumber_pow, lt_translationNumber_of_forall_add_lt, translationNumber_eq_int_iff, le_translationNumber_of_add_nat_le, translationNumber_mono, tendsto_translation_number₀', tendsto_translationNumber_of_dist_bounded_aux, translationNumber_zpow
transnumAuxSeq 📖	CompOp	4 math math: tendsto_translationNumber_aux, transnumAuxSeq_dist_lt, transnumAuxSeq_zero, transnumAuxSeq_def
unitsHasCoeToFun 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ceil_map_map_zero_le 📖	mathematical	—	Int.ceil Real Real.instRing Real.linearOrder Real.instFloorRing DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instZero	—	Int.ceil_mono map_map_zero_le Int.ceil_add_intCast Real.instIsStrictOrderedRing
coe_mk 📖	mathematical	OrderHom.toFun Real Real.instPreorder Real.instAdd Real.instOne	DFunLike.coe CircleDeg1Lift instFunLikeReal OrderHom OrderHom.instFunLike	—	—
coe_mul 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	—
coe_one 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	—
coe_pow 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Monoid.toNatPow instMonoid Nat.iterate	—	pow_succ
coe_toOrderHom 📖	mathematical	—	DFunLike.coe OrderHom Real Real.instPreorder OrderHom.instFunLike toOrderHom CircleDeg1Lift instFunLikeReal	—	—
coe_toOrderIso 📖	mathematical	—	DFunLike.coe OrderIso Real Real.instLE instFunLikeOrderIso MonoidHom Units CircleDeg1Lift instMonoid MulOneClass.toMulOne Units.instMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid RelIso.instGroup MonoidHom.instFunLike toOrderIso instFunLikeReal Units.val	—	—
coe_toOrderIso_inv 📖	mathematical	—	DFunLike.coe OrderIso Real Real.instLE instFunLikeOrderIso InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid RelIso.instGroup MonoidHom Units CircleDeg1Lift instMonoid MulOneClass.toMulOne Units.instMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike toOrderIso instFunLikeReal Units.val Units.instInv	—	—
coe_toOrderIso_symm 📖	mathematical	—	DFunLike.coe OrderIso Real Real.instLE instFunLikeOrderIso OrderIso.symm MonoidHom Units CircleDeg1Lift instMonoid MulOneClass.toMulOne Units.instMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid RelIso.instGroup MonoidHom.instFunLike toOrderIso instFunLikeReal Units.val Units.instInv	—	—
commute_add_int 📖	mathematical	—	Function.Commute Real DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd Real.instIntCast	—	commute_add_nat Int.cast_negSucc Nat.cast_add Nat.cast_one neg_add_rev sub_eq_add_neg commute_sub_nat
commute_add_nat 📖	mathematical	—	Function.Commute Real DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd Real.instNatCast	—	add_comm commute_nat_add
commute_iff_commute 📖	mathematical	—	Commute CircleDeg1Lift MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid Function.Commute Real DFunLike.coe instFunLikeReal	—	ext_iff
commute_int_add 📖	mathematical	—	Function.Commute Real DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd Real.instIntCast	—	add_comm commute_add_int
commute_nat_add 📖	mathematical	—	Function.Commute Real DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd Real.instNatCast	—	add_left_iterate nsmul_one Function.Commute.iterate_right map_one_add
commute_sub_int 📖	mathematical	—	Function.Commute Real DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instSub Real.instIntCast	—	sub_eq_add_neg Function.Semiconj.inverses_right commute_add_int Equiv.right_inv Equiv.left_inv
commute_sub_nat 📖	mathematical	—	Function.Commute Real DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instSub Real.instNatCast	—	sub_eq_add_neg Function.Semiconj.inverses_right commute_add_nat Equiv.right_inv Equiv.left_inv
continuous_iff_surjective 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe CircleDeg1Lift instFunLikeReal	—	Continuous.surjective instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing OrderTopology.to_orderClosedTopology tendsto_atTop tendsto_atBot Monotone.continuous_of_surjective monotone
continuous_pow 📖	mathematical	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe CircleDeg1Lift instFunLikeReal	Monoid.toNatPow instMonoid	—	coe_pow Continuous.iterate
dist_map_map_zero_lt 📖	mathematical	—	Real Real.instLT Dist.dist PseudoMetricSpace.toDist Real.pseudoMetricSpace Real.instAdd DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instZero Real.instOne	—	dist_comm Real.dist_eq abs_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add lt_sub_iff_add_lt' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd sub_lt_iff_lt_add' sub_eq_add_neg lt_map_map_zero map_map_zero_lt
dist_map_zero_lt_of_semiconj 📖	mathematical	Function.Semiconj Real DFunLike.coe CircleDeg1Lift instFunLikeReal	Real.instLT Dist.dist PseudoMetricSpace.toDist Real.pseudoMetricSpace Real.instZero instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat dist_triangle Function.Semiconj.eq sub_sub_eq_add_sub sub_sub add_comm abs_sub_comm add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add dist_map_map_zero_lt one_add_one_eq_two
dist_map_zero_lt_of_semiconjBy 📖	mathematical	SemiconjBy CircleDeg1Lift MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	Real Real.instLT Dist.dist PseudoMetricSpace.toDist Real.pseudoMetricSpace DFunLike.coe instFunLikeReal Real.instZero instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	dist_map_zero_lt_of_semiconj semiconjBy_iff_semiconj
dist_map_zero_translationNumber_le 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist Real.pseudoMetricSpace DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instZero translationNumber Real.instOne	—	dist_le_of_le_geometric_two_of_tendsto₀ le_of_lt Nat.instAtLeastTwoHAddOfNat transnumAuxSeq_dist_lt tendsto_translationNumber_aux transnumAuxSeq_zero
dist_pow_map_zero_mul_translationNumber_le 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist Real.pseudoMetricSpace DFunLike.coe CircleDeg1Lift instFunLikeReal Monoid.toNatPow instMonoid Real.instZero Real.instMul Real.instNatCast translationNumber Real.instOne	—	dist_map_zero_translationNumber_le translationNumber_pow
exists_eq_add_translationNumber 📖	mathematical	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe CircleDeg1Lift instFunLikeReal	Real.instAdd translationNumber	—	lt_irrefl lt_translationNumber_of_forall_add_lt translationNumber_lt_of_forall_lt_add intermediate_value_univ₂ OrderTopology.to_orderClosedTopology instOrderTopologyReal ordered_connected_space LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Continuous.fun_add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_id' continuous_const
ext 📖	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal	—	ext
floor_map_map_zero_le 📖	mathematical	—	Int.floor Real Real.instRing Real.linearOrder Real.instFloorRing DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instZero Int.ceil	—	Int.floor_mono map_map_zero_le Int.floor_add_intCast Real.instIsStrictOrderedRing
floor_sub_le_translationNumber 📖	mathematical	—	Real Real.instLE Real.instIntCast Int.floor Real.instRing Real.linearOrder Real.instFloorRing Real.instSub DFunLike.coe CircleDeg1Lift instFunLikeReal translationNumber	—	le_translationNumber_of_add_int_le le_sub_iff_add_le' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Int.floor_le
forall_map_sub_of_Icc 📖	—	Real Real.instSub DFunLike.coe CircleDeg1Lift instFunLikeReal	—	—	Int.fract_nonneg Real.instIsStrictOrderedRing le_of_lt Int.fract_lt_one map_fract_sub_fract_eq
inf_apply 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal SemilatticeInf.toMin Lattice.toSemilatticeInf instLattice Real.instMin	—	—
instOrderHomClassReal 📖	mathematical	—	OrderHomClass CircleDeg1Lift Real Real.instLE instFunLikeReal	—	OrderHom.monotone'
isUnit_iff_bijective 📖	mathematical	—	IsUnit CircleDeg1Lift instMonoid Function.Bijective Real DFunLike.coe instFunLikeReal	—	OrderIso.bijective Units.isUnit StrictMono.le_iff_le strictMono_iff_injective Equiv.ofBijective_apply_symm_apply map_add_one ext Equiv.ofBijective_symm_apply_apply
iterate_eq_of_map_eq_add_int 📖	mathematical	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Real.instAdd Real.instIntCast	Nat.iterate Real.instMul Real.instNatCast	—	add_right_iterate nsmul_eq_mul Function.Commute.iterate_eq_of_map_eq commute_add_int
iterate_le_of_map_le_add_int 📖	mathematical	Real Real.instLE DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd Real.instIntCast	Nat.iterate Real.instMul Real.instNatCast	—	add_right_iterate nsmul_eq_mul Function.Commute.iterate_le_of_map_le commute_add_int monotone Monotone.add_const covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid monotone_id
iterate_mono 📖	mathematical	CircleDeg1Lift Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLattice	Pi.hasLe Real Real.instLE Nat.iterate DFunLike.coe instFunLikeReal	—	iterate_monotone
iterate_monotone 📖	mathematical	—	Monotone CircleDeg1Lift PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLattice Pi.preorder Real Real.instPreorder Nat.iterate DFunLike.coe instFunLikeReal	—	Monotone.iterate_le_of_le monotone
iterate_pos_eq_iff 📖	mathematical	—	Nat.iterate Real DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd Real.instMul Real.instNatCast Real.instIntCast	—	add_right_iterate nsmul_eq_mul Function.Commute.iterate_pos_eq_iff_map_eq commute_add_int monotone StrictMono.add_const IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid strictMono_id
iterate_pos_le_iff 📖	mathematical	—	Real Real.instLE Nat.iterate DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd Real.instMul Real.instNatCast Real.instIntCast	—	add_right_iterate nsmul_eq_mul Function.Commute.iterate_pos_le_iff_map_le commute_add_int monotone StrictMono.add_const IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid strictMono_id
iterate_pos_lt_iff 📖	mathematical	—	Real Real.instLT Nat.iterate DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd Real.instMul Real.instNatCast Real.instIntCast	—	add_right_iterate nsmul_eq_mul Function.Commute.iterate_pos_lt_iff_map_lt commute_add_int monotone StrictMono.add_const IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid strictMono_id
le_ceil_map_map_zero 📖	mathematical	—	Int.ceil Real Real.instRing Real.linearOrder Real.instFloorRing DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instZero Int.floor MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	Int.ceil_add_intCast Real.instIsStrictOrderedRing Int.ceil_mono le_map_map_zero
le_floor_map_map_zero 📖	mathematical	—	Int.floor Real Real.instRing Real.linearOrder Real.instFloorRing DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instZero	—	Int.floor_add_intCast Real.instIsStrictOrderedRing Int.floor_mono le_map_map_zero
le_iterate_of_add_int_le_map 📖	mathematical	Real Real.instLE Real.instAdd Real.instIntCast DFunLike.coe CircleDeg1Lift instFunLikeReal	Real.instMul Real.instNatCast Nat.iterate	—	add_right_iterate nsmul_eq_mul Function.Commute.iterate_le_of_map_le Function.Commute.symm commute_add_int Monotone.add_const covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid monotone_id monotone
le_iterate_pos_iff 📖	mathematical	—	Real Real.instLE Real.instAdd Real.instMul Real.instNatCast Real.instIntCast Nat.iterate DFunLike.coe CircleDeg1Lift instFunLikeReal	—	iterate_pos_lt_iff
le_map_map_zero 📖	mathematical	—	Real Real.instLE Real.instAdd DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instZero Real.instIntCast Int.floor Real.instRing Real.linearOrder Real.instFloorRing	—	le_map_of_map_zero
le_map_of_map_zero 📖	mathematical	—	Real Real.instLE Real.instAdd DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instZero Real.instIntCast Int.floor Real.instRing Real.linearOrder Real.instFloorRing	—	map_int_of_map_zero monotone Int.floor_le
le_translationNumber_of_add_int_le 📖	mathematical	Real Real.instLE Real.instAdd Real.instIntCast DFunLike.coe CircleDeg1Lift instFunLikeReal	translationNumber	—	ge_of_tendsto' instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_translation_number' le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Nat.cast_add_one_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero le_sub_iff_add_le' mul_comm coe_pow le_iterate_of_add_int_le_map
le_translationNumber_of_add_le 📖	mathematical	Real Real.instLE Real.instAdd DFunLike.coe CircleDeg1Lift instFunLikeReal	translationNumber	—	translationNumber_mono Eq.trans_le add_comm translationNumber_translate
le_translationNumber_of_add_nat_le 📖	mathematical	Real Real.instLE Real.instAdd Real.instNatCast DFunLike.coe CircleDeg1Lift instFunLikeReal	translationNumber	—	le_translationNumber_of_add_int_le
lt_iterate_pos_iff 📖	mathematical	—	Real Real.instLT Real.instAdd Real.instMul Real.instNatCast Real.instIntCast Nat.iterate DFunLike.coe CircleDeg1Lift instFunLikeReal	—	iterate_pos_le_iff
lt_map_map_zero 📖	mathematical	—	Real Real.instLT Real.instSub Real.instAdd DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instZero Real.instOne	—	add_sub_assoc add_lt_add_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Int.sub_one_lt_floor Real.instIsStrictOrderedRing le_map_map_zero
lt_map_of_int_lt_translationNumber 📖	mathematical	Real Real.instLT Real.instIntCast translationNumber	Real.instAdd DFunLike.coe CircleDeg1Lift instFunLikeReal	—	not_le translationNumber_le_of_le_add_int
lt_map_of_nat_lt_translationNumber 📖	mathematical	Real Real.instLT Real.instNatCast translationNumber	Real.instAdd DFunLike.coe CircleDeg1Lift instFunLikeReal	—	lt_map_of_int_lt_translationNumber
lt_translationNumber_of_forall_add_lt 📖	mathematical	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instLT Real.instAdd	translationNumber	—	IsCompact.exists_isMinOn instClosedIicTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal CompactIccSpace.isCompact_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace Set.nonempty_Icc zero_le_one Real.instZeroLEOneClass Continuous.continuousOn Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuous_id lt_of_lt_of_le lt_sub_iff_add_lt' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_translationNumber_of_add_le forall_map_sub_of_Icc
map_add_int 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Real.instAdd Real.instIntCast	—	commute_add_int
map_add_nat 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Real.instAdd Real.instNatCast	—	map_add_int
map_add_one 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Real.instAdd Real.instOne	—	map_add_one'
map_add_one' 📖	mathematical	—	OrderHom.toFun Real Real.instPreorder toOrderHom Real.instAdd Real.instOne	—	—
map_fract_sub_fract_eq 📖	mathematical	—	Real Real.instSub DFunLike.coe CircleDeg1Lift instFunLikeReal Int.fract Real.instRing Real.linearOrder Real.instFloorRing	—	Int.fract.eq_1 map_sub_int sub_sub_sub_cancel_right
map_int_add 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Real.instAdd Real.instIntCast	—	commute_int_add
map_int_of_map_zero 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Real.instIntCast Real.instAdd Real.instZero	—	map_add_int zero_add
map_le_of_map_zero 📖	mathematical	—	Real Real.instLE DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd Real.instZero Real.instIntCast Int.ceil Real.instRing Real.linearOrder Real.instFloorRing	—	monotone Int.le_ceil map_int_of_map_zero
map_lt_add_floor_translationNumber_add_one 📖	mathematical	—	Real Real.instLT DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd Real.instIntCast Int.floor Real.instRing Real.linearOrder Real.instFloorRing translationNumber Real.instOne	—	add_assoc Nat.cast_one Int.cast_one map_lt_of_translationNumber_lt_int Int.cast_add Int.lt_floor_add_one
map_lt_add_translationNumber_add_one 📖	mathematical	—	Real Real.instLT DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd translationNumber Real.instOne	—	map_lt_add_floor_translationNumber_add_one add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_le_add_right Int.floor_le
map_lt_of_translationNumber_lt_int 📖	mathematical	Real Real.instLT translationNumber Real.instIntCast	DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd	—	not_le le_translationNumber_of_add_int_le
map_lt_of_translationNumber_lt_nat 📖	mathematical	Real Real.instLT translationNumber Real.instNatCast	DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd	—	map_lt_of_translationNumber_lt_int
map_map_zero_le 📖	mathematical	—	Real Real.instLE DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instZero Real.instAdd Real.instIntCast Int.ceil Real.instRing Real.linearOrder Real.instFloorRing	—	map_le_of_map_zero
map_map_zero_lt 📖	mathematical	—	Real Real.instLT DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instZero Real.instAdd Real.instOne	—	map_map_zero_le add_lt_add_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Int.ceil_lt_add_one Real.instIsStrictOrderedRing add_assoc
map_nat_add 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Real.instAdd Real.instNatCast	—	map_int_add
map_one_add 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Real.instAdd Real.instOne	—	add_comm map_add_one
map_sub_int 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Real.instSub Real.instIntCast	—	commute_sub_int
map_sub_nat 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Real.instSub Real.instNatCast	—	map_sub_int
mono 📖	mathematical	Real Real.instLE	DFunLike.coe CircleDeg1Lift instFunLikeReal	—	monotone
monotone 📖	mathematical	—	Monotone Real Real.instPreorder DFunLike.coe CircleDeg1Lift instFunLikeReal	—	OrderHom.monotone'
mul_apply 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	—
mul_floor_map_zero_le_floor_iterate_zero 📖	mathematical	—	Int.floor Real Real.instRing Real.linearOrder Real.instFloorRing DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instZero Nat.iterate	—	Int.le_floor Int.cast_mul Int.cast_natCast zero_add le_iterate_of_add_int_le_map
pow_mono 📖	mathematical	CircleDeg1Lift Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLattice	Monoid.toNatPow instMonoid	—	coe_pow iterate_mono
pow_monotone 📖	mathematical	—	Monotone CircleDeg1Lift PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLattice Monoid.toNatPow instMonoid	—	pow_mono
semiconjBy_iff_semiconj 📖	mathematical	—	SemiconjBy CircleDeg1Lift MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid Function.Semiconj Real DFunLike.coe instFunLikeReal	—	ext_iff
semiconj_of_bijective_of_translationNumber_eq 📖	mathematical	Function.Bijective Real DFunLike.coe CircleDeg1Lift instFunLikeReal translationNumber	Function.Semiconj	—	semiconj_of_isUnit_of_translationNumber_eq isUnit_iff_bijective
semiconj_of_group_action_of_forall_translationNumber_eq 📖	mathematical	translationNumber DFunLike.coe MonoidHom CircleDeg1Lift MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instMonoid MonoidHom.instFunLike	Function.Semiconj Real instFunLikeReal	—	Nat.instAtLeastTwoHAddOfNat MonoidHom.coe_toHomUnits map_inv MonoidHom.instMonoidHomClass translationNumber_units_inv mono LT.lt.le map_lt_add_translationNumber_add_one map_add_one le_imp_le_of_le_of_le add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_of_lt le_refl add_assoc add_neg_cancel add_zero one_add_one_eq_two ciSup_mono Monotone.map_ciSup_of_continuousAt instOrderTopologyReal OrderTopology.to_orderClosedTopology One.instNonempty ContinuousAt.fun_add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuousAt_id' continuousAt_const Monotone.add_const monotone_id Function.csSup_div_semiconj
semiconj_of_isUnit_of_translationNumber_eq 📖	mathematical	IsUnit CircleDeg1Lift instMonoid translationNumber	Function.Semiconj Real DFunLike.coe instFunLikeReal	—	units_semiconj_of_translationNumber_eq
strictMono_iff_injective 📖	mathematical	—	StrictMono Real Real.instPreorder DFunLike.coe CircleDeg1Lift instFunLikeReal	—	Monotone.strictMono_iff_injective monotone
sup_apply 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal SemilatticeSup.toMax Lattice.toSemilatticeSup instLattice Real.instMax	—	—
tendsto_atBot 📖	mathematical	—	Filter.Tendsto Real DFunLike.coe CircleDeg1Lift instFunLikeReal Filter.atBot Real.instPreorder	—	Filter.tendsto_atBot_mono map_le_of_map_zero Filter.tendsto_atBot_add_const_left Real.instIsOrderedAddMonoid LT.lt.le Int.ceil_lt_add_one Real.instIsStrictOrderedRing Filter.tendsto_atBot_add_const_right Filter.tendsto_id
tendsto_atTop 📖	mathematical	—	Filter.Tendsto Real DFunLike.coe CircleDeg1Lift instFunLikeReal Filter.atTop Real.instPreorder	—	Filter.tendsto_atTop_mono le_map_of_map_zero Filter.tendsto_atTop_add_const_left Real.instIsOrderedAddMonoid LT.lt.le Int.sub_one_lt_floor Real.instIsStrictOrderedRing sub_eq_add_neg Filter.tendsto_atTop_add_const_right Filter.tendsto_id
tendsto_translationNumber 📖	mathematical	—	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub DFunLike.coe CircleDeg1Lift instFunLikeReal Monoid.toNatPow instMonoid Real.instNatCast Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace translationNumber	—	translationNumber_conj_eq' Filter.Tendsto.congr Units.conj_pow' add_zero sub_eq_neg_add tendsto_translation_number₀
tendsto_translationNumber_aux 📖	mathematical	—	Filter.Tendsto Real transnumAuxSeq Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace translationNumber	—	CauchySeq.tendsto_limUnder Real.instCompleteSpace cauchySeq_of_le_geometric_two le_of_lt Nat.instAtLeastTwoHAddOfNat transnumAuxSeq_dist_lt
tendsto_translationNumber_of_dist_bounded_aux 📖	mathematical	Real Real.instLE Dist.dist PseudoMetricSpace.toDist Real.pseudoMetricSpace DFunLike.coe CircleDeg1Lift instFunLikeReal Monoid.toNatPow instMonoid Real.instZero	Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid Nat.instMonoid Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace translationNumber	—	Filter.Tendsto.congr_dist Nat.instAtLeastTwoHAddOfNat tendsto_translationNumber_aux squeeze_zero dist_nonneg pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass zero_lt_two NeZero.charZero_one IsStrictOrderedRing.toCharZero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid transnumAuxSeq.eq_1 Real.dist_eq sub_div abs_div abs_of_pos div_le_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_const_nhds MulZeroClass.mul_zero Filter.Tendsto.comp tendsto_inv_atTop_zero instOrderTopologyReal tendsto_pow_atTop_atTop_of_one_lt AddGroup.existsAddOfLE Real.instArchimedean one_lt_two IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd
tendsto_translation_number' 📖	mathematical	—	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub DFunLike.coe CircleDeg1Lift instFunLikeReal Monoid.toNatPow instMonoid Real.instAdd Real.instNatCast Real.instOne Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace translationNumber	—	Nat.cast_one Filter.tendsto_add_atTop_iff_nat tendsto_translationNumber
tendsto_translation_number₀ 📖	mathematical	—	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid DFunLike.coe CircleDeg1Lift instFunLikeReal Monoid.toNatPow instMonoid Real.instZero Real.instNatCast Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace translationNumber	—	Filter.tendsto_add_atTop_iff_nat Nat.cast_zero Nat.cast_one tendsto_translation_number₀'
tendsto_translation_number₀' 📖	mathematical	—	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid DFunLike.coe CircleDeg1Lift instFunLikeReal Monoid.toNatPow instMonoid Real.instZero Real.instAdd Real.instNatCast Real.instOne Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace translationNumber	—	tendsto_iff_dist_tendsto_zero squeeze_zero dist_nonneg Nat.cast_add_one_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Real.dist_eq div_sub' ne_of_gt abs_div abs_of_pos Nat.cast_add_one div_le_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono dist_pow_map_zero_mul_translationNumber_le Filter.Tendsto.comp tendsto_const_div_atTop_nhds_zero_nat NNRat.instContinuousSMulOfIsScalarTowerOfRat IsScalarTower.nnrat Rat.instCharZero NNRat.instContinuousSMulRatReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.tendsto_add_atTop_nat
translate_apply 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Units.val instMonoid MonoidHom Multiplicative Units MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass Real.instAddMonoid Units.instMulOneClass MonoidHom.instFunLike translate Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd Real.instAdd	—	—
translate_inv_apply 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Units.val instMonoid Units Units.instInv MonoidHom Multiplicative MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass Real.instAddMonoid Units.instMulOneClass MonoidHom.instFunLike translate Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd Real.instAdd Real.instNeg	—	—
translate_iterate 📖	mathematical	—	Nat.iterate Real DFunLike.coe CircleDeg1Lift instFunLikeReal Units.val instMonoid MonoidHom Multiplicative Units MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass Real.instAddMonoid Units.instMulOneClass MonoidHom.instFunLike translate Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd Real.instMul Real.instNatCast	—	coe_pow Units.val_pow_eq_pow_val translate_pow
translate_pow 📖	mathematical	—	Units CircleDeg1Lift instMonoid Monoid.toNatPow Units.instMonoid DFunLike.coe MonoidHom Multiplicative Real MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass Real.instAddMonoid Units.instMulOneClass MonoidHom.instFunLike translate Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd Real.instMul Real.instNatCast	—	translate_zpow
translate_zpow 📖	mathematical	—	Units CircleDeg1Lift instMonoid DivInvMonoid.toZPow Units.instDivInvMonoid DFunLike.coe MonoidHom Multiplicative Real MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass Real.instAddMonoid Units.instMulOneClass MonoidHom.instFunLike translate Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd Real.instMul Real.instIntCast	—	map_zpow MonoidHom.instMonoidHomClass
translationNumber_conj_eq 📖	mathematical	—	translationNumber CircleDeg1Lift MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid Units.val Units Units.instInv	—	translationNumber_eq_of_semiconjBy Units.mk_semiconjBy
translationNumber_conj_eq' 📖	mathematical	—	translationNumber CircleDeg1Lift MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid Units.val Units Units.instInv	—	translationNumber_conj_eq
translationNumber_eq_int_iff 📖	mathematical	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe CircleDeg1Lift instFunLikeReal	translationNumber Real.instIntCast Real.instAdd	—	exists_eq_add_translationNumber translationNumber_of_eq_add_int
translationNumber_eq_of_dist_bounded 📖	mathematical	Real Real.instLE Dist.dist PseudoMetricSpace.toDist Real.pseudoMetricSpace DFunLike.coe CircleDeg1Lift instFunLikeReal Monoid.toNatPow instMonoid Real.instZero	translationNumber	—	translationNumber_eq_of_tendsto_aux tendsto_translationNumber_of_dist_bounded_aux
translationNumber_eq_of_semiconj 📖	mathematical	Function.Semiconj Real DFunLike.coe CircleDeg1Lift instFunLikeReal	translationNumber	—	translationNumber_eq_of_semiconjBy semiconjBy_iff_semiconj
translationNumber_eq_of_semiconjBy 📖	mathematical	SemiconjBy CircleDeg1Lift MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	translationNumber	—	translationNumber_eq_of_dist_bounded Nat.instAtLeastTwoHAddOfNat le_of_lt dist_map_zero_lt_of_semiconjBy SemiconjBy.pow_right
translationNumber_eq_of_tendsto_aux 📖	mathematical	Filter.Tendsto Real transnumAuxSeq Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	translationNumber	—	Filter.Tendsto.limUnder_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat
translationNumber_eq_of_tendsto₀ 📖	mathematical	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Nat.iterate DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instZero Real.instNatCast Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	translationNumber	—	translationNumber_eq_of_tendsto_aux Nat.instAtLeastTwoHAddOfNat coe_pow Nat.cast_pow Filter.Tendsto.comp tendsto_pow_atTop_atTop_of_one_lt Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd instArchimedeanNat one_lt_two Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
translationNumber_eq_of_tendsto₀' 📖	mathematical	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Nat.iterate DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instZero Real.instAdd Real.instNatCast Real.instOne Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	translationNumber	—	translationNumber_eq_of_tendsto₀ Filter.tendsto_add_atTop_iff_nat Nat.cast_zero Nat.cast_one
translationNumber_eq_rat_iff 📖	mathematical	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe CircleDeg1Lift instFunLikeReal	translationNumber DivInvMonoid.toDiv Real.instDivInvMonoid Real.instIntCast Real.instNatCast Monoid.toNatPow instMonoid Real.instAdd	—	eq_div_iff ne_of_gt Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial mul_comm translationNumber_pow translationNumber_eq_int_iff continuous_pow
translationNumber_le_ceil_sub 📖	mathematical	—	Real Real.instLE translationNumber Real.instIntCast Int.ceil Real.instRing Real.linearOrder Real.instFloorRing Real.instSub DFunLike.coe CircleDeg1Lift instFunLikeReal	—	translationNumber_le_of_le_add_int sub_le_iff_le_add' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Int.le_ceil
translationNumber_le_of_le_add 📖	mathematical	Real Real.instLE DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd	translationNumber	—	translationNumber_mono LE.le.trans_eq add_comm translationNumber_translate
translationNumber_le_of_le_add_int 📖	mathematical	Real Real.instLE DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd Real.instIntCast	translationNumber	—	le_of_tendsto' instClosedIicTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_translation_number' div_le_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_add_one_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero sub_le_iff_le_add' iterate_le_of_map_le_add_int Nat.cast_add_one coe_pow
translationNumber_le_of_le_add_nat 📖	mathematical	Real Real.instLE DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instAdd Real.instNatCast	translationNumber	—	translationNumber_le_of_le_add_int
translationNumber_lt_of_forall_lt_add 📖	mathematical	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe CircleDeg1Lift instFunLikeReal Real.instLT Real.instAdd	translationNumber	—	IsCompact.exists_isMaxOn instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal CompactIccSpace.isCompact_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace Set.nonempty_Icc zero_le_one Real.instZeroLEOneClass Continuous.continuousOn Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuous_id lt_of_le_of_lt translationNumber_le_of_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid forall_map_sub_of_Icc sub_lt_iff_lt_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd
translationNumber_mono 📖	mathematical	—	Monotone CircleDeg1Lift Real PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLattice Real.instPreorder translationNumber	—	le_of_tendsto_of_tendsto' OrderTopology.to_orderClosedTopology instOrderTopologyReal Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_translation_number₀ div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing pow_mono Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass
translationNumber_mul_of_commute 📖	mathematical	Commute CircleDeg1Lift MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	translationNumber Real Real.instAdd	—	tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_translationNumber_of_dist_bounded_aux Commute.mul_pow dist_comm le_of_lt dist_map_map_zero_lt Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_translationNumber_aux
translationNumber_of_eq_add_int 📖	mathematical	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Real.instAdd Real.instIntCast	translationNumber	—	le_antisymm translationNumber_le_of_le_add_int le_of_eq le_translationNumber_of_add_int_le
translationNumber_of_map_pow_eq_add_int 📖	mathematical	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Monoid.toNatPow instMonoid Real.instAdd Real.instIntCast	translationNumber DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast	—	translationNumber_of_eq_add_int eq_div_iff Nat.cast_ne_zero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing ne_of_gt mul_comm translationNumber_pow
translationNumber_one 📖	mathematical	—	translationNumber CircleDeg1Lift MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass instMonoid Real Real.instZero	—	translationNumber_eq_of_tendsto₀ Function.iterate_id zero_div T5Space.toT1Space OrderTopology.t5Space instOrderTopologyReal Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat
translationNumber_pow 📖	mathematical	—	translationNumber CircleDeg1Lift Monoid.toNatPow instMonoid Real Real.instMul Real.instNatCast	—	pow_zero translationNumber_one CharP.cast_eq_zero CharP.ofCharZero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing MulZeroClass.zero_mul pow_succ translationNumber_mul_of_commute Commute.pow_self Nat.cast_add_one add_mul Distrib.rightDistribClass one_mul
translationNumber_translate 📖	mathematical	—	translationNumber Units.val CircleDeg1Lift instMonoid DFunLike.coe MonoidHom Multiplicative Real Units MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass Real.instAddMonoid Units.instMulOneClass MonoidHom.instFunLike translate Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	translationNumber_eq_of_tendsto₀' translate_iterate Nat.cast_succ add_zero mul_div_cancel_left₀ GroupWithZero.toMulDivCancelClass Nat.cast_add_one_ne_zero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
translationNumber_units_inv 📖	mathematical	—	translationNumber Units.val CircleDeg1Lift instMonoid Units Units.instInv Real Real.instNeg	—	eq_neg_iff_add_eq_zero translationNumber_mul_of_commute Commute.units_inv_left Commute.refl Units.inv_mul translationNumber_one
translationNumber_zpow 📖	mathematical	—	translationNumber Units.val CircleDeg1Lift instMonoid Units DivInvMonoid.toZPow Units.instDivInvMonoid Real Real.instMul Real.instIntCast	—	zpow_natCast translationNumber_pow Int.cast_natCast zpow_negSucc Nat.cast_add Nat.cast_one translationNumber_units_inv mul_neg Int.cast_negSucc neg_add_rev Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_one
transnumAuxSeq_def 📖	mathematical	—	transnumAuxSeq Real DivInvMonoid.toDiv Real.instDivInvMonoid DFunLike.coe CircleDeg1Lift instFunLikeReal Monoid.toNatPow instMonoid Nat.instMonoid Real.instZero Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	—
transnumAuxSeq_dist_lt 📖	mathematical	—	Real Real.instLT Dist.dist PseudoMetricSpace.toDist Real.pseudoMetricSpace transnumAuxSeq DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow Real.instMonoid	—	Nat.instAtLeastTwoHAddOfNat pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass zero_lt_two NeZero.charZero_one IsStrictOrderedRing.toCharZero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_div pow_succ' abs_of_pos abs_div sub_div pow_succ two_mul mul_div_mul_left two_ne_zero' CharZero.NeZero.two pow_mul sq mul_apply div_lt_div_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono dist_map_map_zero_lt abs_pos_of_pos IsStrictOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo
transnumAuxSeq_zero 📖	mathematical	—	transnumAuxSeq DFunLike.coe CircleDeg1Lift Real instFunLikeReal Real.instZero	—	pow_zero pow_one div_one
units_apply_inv_apply 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Units.val instMonoid Units Units.instInv	—	Units.mul_inv
units_inv_apply_apply 📖	mathematical	—	DFunLike.coe CircleDeg1Lift Real instFunLikeReal Units.val instMonoid Units Units.instInv	—	Units.inv_mul
units_semiconj_of_translationNumber_eq 📖	mathematical	translationNumber Units.val CircleDeg1Lift instMonoid	Function.Semiconj Real DFunLike.coe instFunLikeReal	—	translationNumber_zpow zpow_one semiconj_of_group_action_of_forall_translationNumber_eq

(root)

Definitions

Name	Category	Theorems
CircleDeg1Lift 📖	CompData	88 math math: CircleDeg1Lift.mono, CircleDeg1Lift.units_inv_apply_apply, CircleDeg1Lift.instOrderHomClassReal, CircleDeg1Lift.translate_inv_apply, CircleDeg1Lift.map_sub_int, CircleDeg1Lift.map_add_nat, CircleDeg1Lift.commute_nat_add, CircleDeg1Lift.iterate_pos_le_iff, CircleDeg1Lift.iterate_pos_lt_iff, CircleDeg1Lift.isUnit_iff_bijective, CircleDeg1Lift.commute_iff_commute, CircleDeg1Lift.dist_map_zero_translationNumber_le, CircleDeg1Lift.map_lt_add_floor_translationNumber_add_one, CircleDeg1Lift.tendsto_atBot, CircleDeg1Lift.translationNumber_one, CircleDeg1Lift.strictMono_iff_injective, CircleDeg1Lift.floor_sub_le_translationNumber, CircleDeg1Lift.map_one_add, CircleDeg1Lift.map_le_of_map_zero, CircleDeg1Lift.le_map_of_map_zero, CircleDeg1Lift.ext_iff, CircleDeg1Lift.dist_map_map_zero_lt, CircleDeg1Lift.inf_apply, CircleDeg1Lift.lt_map_of_nat_lt_translationNumber, CircleDeg1Lift.coe_toOrderIso_symm, CircleDeg1Lift.translate_iterate, CircleDeg1Lift.map_int_of_map_zero, CircleDeg1Lift.coe_toOrderIso_inv, CircleDeg1Lift.units_apply_inv_apply, CircleDeg1Lift.map_map_zero_lt, CircleDeg1Lift.le_floor_map_map_zero, CircleDeg1Lift.coe_mk, CircleDeg1Lift.mul_apply, CircleDeg1Lift.transnumAuxSeq_zero, CircleDeg1Lift.lt_map_of_int_lt_translationNumber, CircleDeg1Lift.tendsto_translation_number', CircleDeg1Lift.map_nat_add, CircleDeg1Lift.commute_add_int, CircleDeg1Lift.continuous_iff_surjective, CircleDeg1Lift.iterate_monotone, CircleDeg1Lift.commute_sub_int, CircleDeg1Lift.commute_add_nat, CircleDeg1Lift.le_map_map_zero, CircleDeg1Lift.map_sub_nat, CircleDeg1Lift.transnumAuxSeq_def, CircleDeg1Lift.coe_mul, CircleDeg1Lift.translate_apply, CircleDeg1Lift.translationNumber_le_ceil_sub, CircleDeg1Lift.dist_pow_map_zero_mul_translationNumber_le, CircleDeg1Lift.coe_toOrderIso, CircleDeg1Lift.translate_zpow, CircleDeg1Lift.map_add_int, CircleDeg1Lift.le_ceil_map_map_zero, CircleDeg1Lift.coe_one, CircleDeg1Lift.commute_int_add, CircleDeg1Lift.lt_iterate_pos_iff, CircleDeg1Lift.tendsto_translation_number₀, CircleDeg1Lift.translationNumber_conj_eq, CircleDeg1Lift.tendsto_atTop, CircleDeg1Lift.lt_map_map_zero, CircleDeg1Lift.sup_apply, CircleDeg1Lift.ceil_map_map_zero_le, CircleDeg1Lift.map_int_add, CircleDeg1Lift.monotone, CircleDeg1Lift.coe_toOrderHom, CircleDeg1Lift.le_iterate_pos_iff, CircleDeg1Lift.pow_monotone, CircleDeg1Lift.map_lt_add_translationNumber_add_one, CircleDeg1Lift.coe_pow, CircleDeg1Lift.translationNumber_conj_eq', CircleDeg1Lift.map_lt_of_translationNumber_lt_nat, CircleDeg1Lift.tendsto_translationNumber, CircleDeg1Lift.translationNumber_translate, CircleDeg1Lift.map_fract_sub_fract_eq, CircleDeg1Lift.translationNumber_units_inv, CircleDeg1Lift.translationNumber_pow, CircleDeg1Lift.floor_map_map_zero_le, CircleDeg1Lift.map_map_zero_le, CircleDeg1Lift.mul_floor_map_zero_le_floor_iterate_zero, CircleDeg1Lift.iterate_pos_eq_iff, CircleDeg1Lift.translate_pow, CircleDeg1Lift.map_add_one, CircleDeg1Lift.commute_sub_nat, CircleDeg1Lift.translationNumber_mono, CircleDeg1Lift.tendsto_translation_number₀', CircleDeg1Lift.translationNumber_zpow, CircleDeg1Lift.semiconjBy_iff_semiconj, CircleDeg1Lift.map_lt_of_translationNumber_lt_int

---

← Back to Index