Commit 2023-02-11 08:36 24c3d9ba

View on Github →

feat: Port/Topology.Partial (#2081) port of topology.partial only basic naming fixes

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Partial.lean

added def Pcontinuous

added theorem continuousWithinAt_iff_ptendsto_res

added theorem open_dom_of_pcontinuous

added theorem pcontinuous_iff'

added theorem ptendsto'_nhds

added theorem ptendsto_nhds

added theorem rtendsto'_nhds

added theorem rtendsto_nhds