Commit 2023-11-29 15:49 d8ade144

View on Github →

chore: rename some lemmas involving "of_closed" (#8492) Three particular examples which caught my eye; not exhaustive.

Estimated changes

Modified Mathlib/MeasureTheory/Function/ContinuousMapDense.lean

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

Modified Mathlib/Topology/CompletelyRegular.lean

Modified Mathlib/Topology/Connected/Basic.lean

deleted theorem IsConnected.preimage_of_closedMap

added theorem IsConnected.preimage_of_isClosedMap

deleted theorem IsPreconnected.preimage_of_closed_map

added theorem IsPreconnected.preimage_of_isClosedMap

Modified Mathlib/Topology/ContinuousFunction/Ideals.lean

Modified Mathlib/Topology/Metrizable/Urysohn.lean

Modified Mathlib/Topology/PartitionOfUnity.lean

Modified Mathlib/Topology/UrysohnsBounded.lean

Modified Mathlib/Topology/UrysohnsLemma.lean

deleted theorem exists_continuous_zero_one_of_closed

added theorem exists_continuous_zero_one_of_isClosed

Modified docs/overview.yaml