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
Le 30/06/2017 à 20:41, Manuel Eberl a écrit :
So what about the suggestion of just writing "strict_mono" instead?
Besides, you can always introduce local abbreviations for things with
"notation" and delete them with "no_notation" afterwards.
strict_mono would be perfectly OK if there is a
r le_cINF_iff)
qed
end
But if one imports Probability instead of Analysis, then compact
becomes the one from Complete_Partial_Order2 (which, I think, is
much less commonly used than the compactness for topological
spaces). Strangely enough, even rep
