Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-15 23:11 1ec48762

View on Github →

chore(topology/*): Fix lint (#16030) Fix the linting errors coming from fintype_finite, to_additive_doc and doc_blame.

Estimated changes

Modified src/order/filter/ultrafilter.lean

added theorem ultrafilter.eq_pure_of_finite

deleted theorem ultrafilter.eq_pure_of_fintype

Modified src/topology/algebra/const_mul_action.lean

Modified src/topology/algebra/constructions.lean

Modified src/topology/algebra/continuous_monoid_hom.lean

Modified src/topology/algebra/filter_basis.lean

Modified src/topology/algebra/group.lean

Modified src/topology/algebra/nonarchimedean/basic.lean

Modified src/topology/algebra/order/compact.lean

modified theorem continuous.exists_forall_le_of_has_compact_mul_support

Modified src/topology/category/Profinite/cofiltered_limit.lean

added theorem Profinite.exists_locally_constant_finite_aux

added theorem Profinite.exists_locally_constant_finite_nonempty

deleted theorem Profinite.exists_locally_constant_fintype_aux

deleted theorem Profinite.exists_locally_constant_fintype_nonempty

Modified src/topology/category/Top/open_nhds.lean

Modified src/topology/constructions.lean

added theorem pi_generate_from_eq_finite

deleted theorem pi_generate_from_eq_fintype

Modified src/topology/separation.lean

modified theorem discrete_of_t1_of_finite

Modified src/topology/uniform_space/completion.lean

modified def Cauchy.extend