Posts Tagged ‘topology’

IsarMathLib 1.9.0 released

July 26, 2013

I have released version 1.9.0 of IsarMathLib. This is a quite large release with 10 new theory files and 155 new theorems, all contributed by Daniel de la Concepción Sáez. The first of the files contributed by Daniel (released in 1.8.0), Topology_ZF_4 about nets, filters and convergence in topological spaces is now presented on the site. The rest of Daniel’s contributions for now can be viewed in the proof document and the outline.

Here is a short description of what is in the new theories:



IsarMathLib 1.7.2

July 20, 2011

I have released a new version of IsarMathLib. It adds about 50 new lemmas, mostly in group theory and topology, leading to the following characterization of closure in topological groups:

\overline{A} = \bigcap_{H\in \mathcal{N}_0} A+H

Here, \mathcal{N}_0 is the collection of neighborhoods of zero (sets whose interior contains the neutral element of the group), and for two sets A,B\subseteq G we define A+B as A+B=\{a+b | a\in A, b\in B\}.