Mathlib v3 is deprecated. Go to Mathlib v4

Theorem uniformity_basis_dist_pow_of_lt_1

Modification history

2022-03-17 06:22
src/analysis/specific_limits/basic.lean
refactor(analysis/specific_limits): split into two files (#12759) …
Modified uniformity_basis_dist_pow_of_lt_1View on Github →
2021-06-11 13:26
src/analysis/specific_limits.lean
feat(analysis): Cauchy sequence and series lemmas (#7858) …
Modified uniformity_basis_dist_pow_of_lt_1View on Github →
2020-11-11 13:39
src/analysis/specific_limits.lean
chore(algebra/archimedean): add `exists_pow_lt_of_lt_1` (#4970)
Added uniformity_basis_dist_pow_of_lt_1View on Github →