[isabelle-dev] Redundant definitions in Analysis

[Sebastien Gouezel]

Le 11/03/2019 à 19:13, Fabian Immler a écrit :
> Sébastien might have a stronger opinion (I don't), but I would also go 
> for continuous_map: it is in line with open_map, closed_map, 
> quotient_map (which we don't have as constants, but use in theorem 
> names). Moreover, we have more occurrences of continuous_map (174+0 vs 
> 83+39 in isabelle+AFP).

You can definitely go for continuous_map.

Best,

Sebastien