Stream: Beginner Questions

Topic: Abstract_topology


view this post on Zulip 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

view this post on Zulip 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!)

view this post on Zulip 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!)

view this post on Zulip 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

view this post on Zulip 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: Sep 25 2022 at 23:25 UTC