Commit 2023-03-29 10:59 a06940b1

View on Github →

feat: forward-port #18321 (#3101)

Estimated changes

Modified Mathlib/Data/Analysis/Topology.lean

Modified Mathlib/Topology/Constructions.lean

deleted theorem continuous_subtype_nhds_cover

Modified Mathlib/Topology/ContinuousFunction/Basic.lean

Modified Mathlib/Topology/ContinuousOn.lean

added theorem continuous_of_cover_nhds

added theorem nhdsWithin_bunionᵢ

modified theorem nhdsWithin_eq_nhds

added theorem nhdsWithin_unionᵢ

added theorem nhdsWithin_unionₛ

Modified Mathlib/Topology/LocallyFinite.lean

modified theorem LocallyFinite.closure_unionᵢ

added theorem LocallyFinite.continuousOn_unionᵢ'

added theorem LocallyFinite.continuousOn_unionᵢ

Modified Mathlib/Topology/SubsetProperties.lean