Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-09 09:39 27929793

View on Github →

chore(topology/*): rename compact_univ to is_compact_univ, and many more (#17436) Many lemma names about compact sets have compact instead of is_compact in their names, for historical reasons. We rename several of them to match more closely the naming convention.

Estimated changes

Modified docs/overview.yaml

Modified docs/undergrad.yaml

Modified roadmap/topology/paracompact.lean

Modified src/algebraic_geometry/morphisms/quasi_compact.lean

Modified src/algebraic_geometry/morphisms/quasi_separated.lean

Modified src/algebraic_geometry/open_immersion.lean

Modified src/algebraic_geometry/prime_spectrum/basic.lean

Modified src/analysis/convex/exposed.lean

Modified src/analysis/convex/krein_milman.lean

Modified src/analysis/convex/topology.lean

deleted theorem compact_std_simplex

added theorem is_compact_std_simplex

Modified src/analysis/convolution.lean

Modified src/analysis/normed_space/algebra.lean

Modified src/analysis/normed_space/compact_operator.lean

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/analysis/normed_space/operator_norm.lean

Modified src/dynamics/omega_limit.lean

Modified src/geometry/manifold/bump_function.lean

deleted theorem smooth_bump_function.closed_image_of_closed

deleted theorem smooth_bump_function.closed_symm_image_closed_ball

added theorem smooth_bump_function.is_closed_image_of_is_closed

added theorem smooth_bump_function.is_closed_symm_image_closed_ball

added theorem smooth_bump_function.is_open_support

deleted theorem smooth_bump_function.open_support

Modified src/geometry/manifold/partition_of_unity.lean

Modified src/measure_theory/constructions/borel_space.lean

Modified src/measure_theory/group/measure.lean

Modified src/measure_theory/measure/haar.lean

Modified src/measure_theory/measure/measure_space.lean

Modified src/topology/alexandroff.lean

Modified src/topology/algebra/group.lean

Modified src/topology/continuous_function/bounded.lean

Modified src/topology/continuous_function/cocompact_map.lean

deleted theorem cocompact_map.compact_preimage

added theorem cocompact_map.is_compact_preimage

Modified src/topology/continuous_function/compact.lean

Modified src/topology/discrete_quotient.lean

Modified src/topology/homeomorph.lean

deleted theorem homeomorph.compact_image

deleted theorem homeomorph.compact_preimage

added theorem homeomorph.is_compact_image

added theorem homeomorph.is_compact_preimage

Modified src/topology/metric_space/antilipschitz.lean

Modified src/topology/metric_space/basic.lean

modified theorem metric.bounded_range_of_tendsto

deleted theorem metric.compact_iff_closed_bounded

added theorem metric.is_compact_iff_is_closed_bounded

Modified src/topology/metric_space/closeds.lean

Modified src/topology/metric_space/gromov_hausdorff.lean

Modified src/topology/metric_space/gromov_hausdorff_realized.lean

Modified src/topology/noetherian_space.lean

Modified src/topology/paracompact.lean

Modified src/topology/separation.lean

deleted theorem compact_closure_of_subset_compact

deleted theorem compact_compact_separated

deleted theorem exists_subset_nhd_of_compact

added theorem exists_subset_nhds_of_is_compact

deleted theorem image_closure_of_compact

added theorem image_closure_of_is_compact

added theorem is_compact_closure_of_subset_compact

added theorem is_compact_is_compact_separated

Modified src/topology/sequences.lean

Modified src/topology/sets/compacts.lean

Modified src/topology/spectral/hom.lean

added theorem is_compact.preimage_of_is_open

deleted theorem is_compact.preimage_of_open

Modified src/topology/stone_cech.lean

Modified src/topology/subset_properties.lean

deleted theorem compact_Union

deleted theorem compact_accumulate

deleted theorem compact_iff_compact_in_subtype

deleted theorem compact_of_is_closed_subset

deleted theorem compact_univ

deleted theorem exists_subset_nhd_of_compact'

deleted theorem exists_subset_nhd_of_compact_space

added theorem exists_subset_nhds_of_compact_space

added theorem exists_subset_nhds_of_is_compact'

deleted theorem finset.compact_bUnion

added theorem finset.is_compact_bUnion

added theorem is_compact_Union

added theorem is_compact_accumulate

added theorem is_compact_iff_is_compact_in_subtype

added theorem is_compact_of_is_closed_subset

added theorem is_compact_univ

deleted theorem set.finite.compact_bUnion

added theorem set.finite.is_compact_bUnion

Modified src/topology/support.lean

Modified src/topology/uniform_space/cauchy.lean

deleted theorem compact_iff_totally_bounded_complete

deleted theorem compact_of_totally_bounded_is_closed

added theorem is_compact_iff_totally_bounded_is_complete

added theorem is_compact_of_totally_bounded_is_closed

Modified src/topology/uniform_space/compact.lean

Modified src/topology/uniform_space/compact_convergence.lean

Modified src/topology/uniform_space/uniform_convergence.lean