# Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

```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
```
```
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
```