Commit 2024-11-14 00:15 946eb8cc

View on Github →

chore: rename second_countable -> secondCountable in lemma and instance names (#18911) While at it, also renames sigma_compact, first_countable and locally_compact, in the same way.

Estimated changes

Modified Counterexamples/SorgenfreyLine.lean

Modified Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

added theorem WithSeminorms.firstCountableTopology

deleted theorem WithSeminorms.first_countable

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

added theorem ChartedSpace.secondCountable_of_sigmaCompact

deleted theorem ChartedSpace.secondCountable_of_sigma_compact

Modified Mathlib/Geometry/Manifold/Metrizable.lean

Modified Mathlib/Topology/Algebra/Group/OpenMapping.lean

Modified Mathlib/Topology/Category/LightProfinite/Basic.lean

Modified Mathlib/Topology/ClopenBox.lean

added theorem TopologicalSpace.Clopens.countable_iff_secondCountable

deleted theorem TopologicalSpace.Clopens.countable_iff_second_countable

modified theorem TopologicalSpace.Clopens.exists_finset_eq_sup_prod

modified theorem TopologicalSpace.Clopens.exists_prod_subset

modified theorem TopologicalSpace.Clopens.surjective_finset_sup_prod

Modified Mathlib/Topology/Compactness/SigmaCompact.lean

added theorem countable_cover_nhdsWithin_of_sigmaCompact

deleted theorem countable_cover_nhdsWithin_of_sigma_compact

added theorem countable_cover_nhds_of_sigmaCompact

deleted theorem countable_cover_nhds_of_sigma_compact

Modified Mathlib/Topology/MetricSpace/ProperSpace.lean

Modified Mathlib/Topology/Metrizable/Urysohn.lean