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

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!)

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!)

@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

@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: Sep 11 2024 at 16:22 UTC