Commit 2023-09-22 11:29 b68cba43

View on Github →

chore(Topology/SubsetProperties): rename isCompact_of_isClosed_subset (#7298) As discussed on Zulip.

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiffDef.lean

Modified Mathlib/Analysis/Convex/Exposed.lean

Modified Mathlib/Analysis/Convex/KreinMilman.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/NormedSpace/Algebra.lean

Modified Mathlib/Analysis/NormedSpace/FiniteDimension.lean

Modified Mathlib/Dynamics/OmegaLimit.lean

Modified Mathlib/Geometry/Manifold/BumpFunction.lean

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

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

Modified Mathlib/Topology/Compactification/OnePoint.lean

Modified Mathlib/Topology/ContinuousFunction/Bounded.lean

Modified Mathlib/Topology/ContinuousFunction/CocompactMap.lean

Modified Mathlib/Topology/MetricSpace/Basic.lean

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean

Modified Mathlib/Topology/ProperMap.lean

Modified Mathlib/Topology/Separation.lean

Modified Mathlib/Topology/SubsetProperties.lean

added theorem IsCompact.of_isClosed_subset

deleted theorem isCompact_of_isClosed_subset

Modified Mathlib/Topology/Support.lean