Adding abstract topology to LISA

[jarctan]

Goal

Add support for abstract topology (with open/closed sets) in LISA

Content

Definitions

• direct image/preimage
• topology
• discrete/indiscrete topology
• mapping (homomorphism of topological spaces)
• continuity
• connectedness
• (open) covers and compactness

Proofs

• Several set theoretical lemmas (in SetTheoryBasics.scala)
• Several lemmas about direct image/preimage (in DirectPreimages.scala)
• Definition of a topology (in Topology.scala)
• Discrete/indiscrete topologies are topologies indeed (in DiscreteTopology.scala)
• Intersection of topology (in Intersection.scala)
• Characterization of the topology containing all the topologies (in SingletonSet.scala)
• Intermediate value theorem (in Continuity.scala)
• Image of a compact space (in Compactness.scala)

How to run

• sbt
• project lisa-topology
• run
• Then choose the numebr of the file you want to run (1-6)