Nicolò Cavalleri (Jun 29 2021 at 10:57): Nicolò Cavalleri (Jun 29 2021 at 10:57):Is there a way to state continuous (at x within X) c with the library Abstract_topology? I can't find any part of it that deals with filters
Nicolò Cavalleri (Jun 30 2021 at 18:30):Similarly I can't find how you express the concept of second countable in this library. I was expecting to find it in the file Lindelof_spaces but apparently the theorem that says that a second countable space is Lindelof is not there! (Weird: I would say it is an important theorem in the theory of second countable spaces!)
Nicolò Cavalleri (Jun 30 2021 at 18:34):In case someone here knows someone else who does not see this forum often but who could know the answer to these questions I would be extremely grateful if I could have their email, as I am kind of stuck until I find out these answers (writing topology API that is already in HOL is very time consuming and counter productive!)
Lawrence Paulson (Jul 01 2021 at 14:22):@Nicolò Cavalleri (at...within...) belongs to the type class world, where continuous is defined WRT a filter and a limit (see continuous_def). The Abstract_Topology predicate continuous_map is defined analogously to the theorem continuous_openin_preimage_eq, so in a less general form. One could presumably define filters in this theory
Nicolò Cavalleri (Jul 01 2021 at 15:47):@Lawrence Paulson thanks for the anser. I was indeed wondering if there was a definition and some related theory somewhere that is not in the files Abstract_topology(_2)(maybe in the Afp?) as I would need to work with it and it would take me a long time to write it from scratch! Are you sure there is no such theory anywhere? In case not do you know someone else who might know?
Last updated: Dec 21 2024 at 16:20 UTC