On the Boundary and Derivative of a Set

Abstract

This is the first Mizar article in a series aiming at a complete formalization of the textbook “General Topology” by Engelking [7]. We cover the first part of Section 1.3, by defining such notions as a derivative of a subset A of a topological space (usually denoted by Ad, but Der A in our notation), the derivative and the boundary of families of subsets, points of accumulation and isolated points. We also introduce dense-in-itself, perfect and scattered topological spaces and formulate the notion of the density of a space. Some basic properties are given as well as selected exercises from [7].