Commit 2023-05-28 08:49 3ff6ded9

View on Github →

chore: rename Pcontinuous to PContinuous (#4428) ref #4354

Estimated changes

Modified Mathlib/Topology/Basic.lean

Modified Mathlib/Topology/Partial.lean

added def PContinuous

deleted def Pcontinuous

modified theorem open_dom_of_pcontinuous