Commit 2024-01-22 17:37 012256be

View on Github →

chore(Topology/Partial): rename type variables (#9862) We use letters X and Y for topological spaces now, not Greek letters.

Estimated changes

modified def PContinuous
modified theorem open_dom_of_pcontinuous
modified theorem pcontinuous_iff'
modified theorem ptendsto'_nhds
modified theorem ptendsto_nhds
modified theorem rtendsto'_nhds
modified theorem rtendsto_nhds