Def Pcontinuous

Modification history

2023-05-28 08:49

Mathlib/Topology/Partial.lean

chore: rename `Pcontinuous` to `PContinuous` (#4428) …

Deleted Pcontinuous View on Github →

2023-02-11 08:36

Mathlib/Topology/Partial.lean

feat: Port/Topology.Partial (#2081) …

Added Pcontinuous View on Github →