Volume 24 (2016): Issue 2 (June 2016)

Formalization of a part of [11]. Unfortunately, not all is possible to be formalized. Namely, in the paper there is a mistake in the proof of Lemma 3. It states that there exists x ∈ M₁ such that M₁(x) > N₁(x) and (∀y ∈ N₁)x ⊀ y. It should be M₁(x) ⩾ N₁(x). Nevertheless we do not know whether x ∈ N₁ or not and cannot prove the contradiction. In the article we referred to [8], [9] and [10].

We formalize, in two different ways, that “the n-dimensional Euclidean metric space is a complete metric space” (version 1. with the results obtained in [13], [26], [25] and version 2., the results obtained in [13], [14], (registrations) [24]).

With the Cantor’s theorem - in complete metric space (proof by Karol Pąk in [22]), we formalize “The Nested Intervals Theorem in 1-dimensional Euclidean metric space”.

Pierre Cousin’s proof in 1892 [18] the lemma, published in 1895 [9] states that:

“Soit, sur le plan YOX, une aire connexe S limitée par un contour fermé simple ou complexe; on suppose qu’à chaque point de S ou de son périmètre correspond un cercle, de rayon non nul, ayant ce point pour centre : il est alors toujours possible de subdiviser S en régions, en nombre fini et assez petites pour que chacune d’elles soit complétement intérieure au cercle correspondant à un point convenablement choisi dans S ou sur son périmètre.”

Cousin’s Lemma, used in Henstock and Kurzweil integral [29] (generalized Riemann integral), state that: “for any gauge δ, there exists at least one δ-fine tagged partition”. In the last section, we formalize this theorem. We use the suggestions given to the Cousin’s Theorem p.11 in [5] and with notations: [4], [29], [19], [28] and [12].

In [21], Marco Riccardi formalized that ℝN-basis n is a basis (in the algebraic sense defined in [26]) of ℰTn${\cal E}_T^n $ and in [20] he has formalized that ℰTn${\cal E}_T^n $ is second-countable, we build (in the topological sense defined in [23]) a denumerable base of ℰTn${\cal E}_T^n $.

Then we introduce the n-dimensional intervals (interval in n-dimensional Euclidean space, pavé (borné) de ℝⁿ[16], semi-intervalle (borné) de ℝⁿ[22]).

We conclude with the definition of Chebyshev distance [11].

Rough sets, developed by Zdzisław Pawlak [12], are an important tool to describe the state of incomplete or partially unknown information. In this article, which is essentially the continuation of [8], we try to give the characterization of approximation operators in terms of ordinary properties of underlying relations (some of them, as serial and mediate relations, were not available in the Mizar Mathematical Library [11]). Here we drop the classical equivalence- and tolerance-based models of rough sets trying to formalize some parts of [18].

The main aim of this Mizar article is to provide a formal counterpart for the rest of the paper of William Zhu [18]. In order to do this, we recall also Theorem 3 from Y.Y. Yao’s paper [17]. The first part of our formalization (covering first seven pages) is contained in [8]. Now we start from page 5003, sec. 3.4. [18]. We formalized almost all numbered items (definitions, propositions, theorems, and corollaries), with the exception of Proposition 7, where we stated our theorem only in terms of singletons. We provided more thorough discussion of the property positive alliance and its connection with seriality and reflexivity (and also transitivity). Examples were not covered as a rule as we tried to construct a more general mechanism of finding appropriate models for approximation spaces in Mizar providing more automatization than it is now [10].

Of course, we can see some more general applications of some registrations of clusters, essentially not dealing with the notion of an approximation: the notions of an alliance binary relation were not defined in the Mizar Mathematical Library before, and we should think about other properties which are also absent but needed in the context of rough approximations [9], [5]. Via theory merging, using mechanisms described in [6] and [7], such elementary constructions can be extended to other frameworks.

In our earlier article [12], the first part of axioms of geometry proposed by Alfred Tarski [14] was formally introduced by means of Mizar proof assistant [9]. We defined a structure TarskiPlane with the following predicates:

of betweenness between (a ternary relation),

In order to show that the structure which satisfies all eleven Tarski’s axioms really exists, we provided a proof of the registration of a cluster that the Euclidean plane, or rather a natural [5] extension of ordinary metric structure Euclid 2 satisfies all these attributes.

Although the tradition of the mechanization of Tarski’s geometry in Mizar is not as long as in Coq [11], first approaches to this topic were done in Mizar in 1990 [16] (even if this article started formal Hilbert axiomatization of geometry, and parallel development was rather unlikely at that time [8]). Connection with another proof assistant should be mentioned – we had some doubts about the proof of the Euclid’s axiom and inspection of the proof taken from Archive of Formal Proofs of Isabelle [10] clarified things a bit. Our development allows for the future faithful mechanization of [13] and opens the possibility of automatically generated Prover9 proofs which was useful in the case of lattice theory [7].