Le 30/06/2017 à 16:57, Manuel Eberl a écrit :

I agree about 90%, I think, but one could argue that "subseq" contains additional meta-information: the semantic meaning is that it is a strictly monotonic function, but the idea behind it is that it describes a sub-sequence of some other sequence.Still, I for one think this is not really worth the trouble of keeping an entirely separate constant around, especially because "subseq h" does not make much sense: "h" itself is not a subsequence of anything, "f ∘ h" is a sub-sequence of "f". It would be interesting to know what other users of Complex_Main think about that.

I used subseq quite heavily in my ergodic theory developments. From a mathematician point of view, taking subsequences of sequences from nat to nat is very common and very useful in analysis (much

`more than taking subsequences of lists). For instance, the fact that a`

`sequence of functions which converges in L^2 has a subsequence which`

`converges everywhere, is extremely powerful. Having to type`

topological_spaces.subseq all the time would be very cumbersome, on the other hand using something like subsequence would be perfectly OK (and I am strongly in favour of keeping it). By the way, I recently encountered a similar (and even more nasty) name clash, with compact. The following works perfectly theory Foo imports Analysis begin lemma infdist_compact_attained: assumes "compact C" "C ≠ {}" shows "∃c∈C. infdist x C = dist x c" proof - have "∃c∈C. ∀d∈C. dist x c ≤ dist x d" by (rule continuous_attains_inf[OF assms], intro continuous_intros) then show ?thesis unfolding infdist_def using `C ≠ {}` by (metis antisym bdd_below_infdist cINF_lower 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 replacing compact with topological_space.compact does not solve the issue. Sebastien Gouezel _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev