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
