On the Characteristic and Weight of a Topological Space 1
Grzegorz Bancerek · 2005
Summary. We continue Mizar formalization of General Topology according to the book [13] by Engelking. In the article the formalization of Section 1.1 is completed. Namely, the paper includes the formalization of theorems on correspondence of the basis and basis in a point, definitions of the character of a point and a topological space, a neighborhood system, and the weight of a topological space. The formalization is tested with almost discrete topological spaces with infinity.