Some authors have formalized the integral in the Mizar Mathematical Library (MML). The first article in a series on the Darboux/Riemann integral was written by Noboru Endou and Artur Korniłowicz: [6]. The Lebesgue integral was formalized a little later [13] and recently the integral of Riemann-Stieltjes was introduced in the MML by Keiko Narita, Kazuhisa Nakasho and Yasunari Shidama [12]. A presentation of definitions of integrals in other proof assistants or proof checkers (ACL2, COQ, Isabelle/HOL, HOL4, HOL Light, PVS, ProofPower) may be found in [10] and [4]. Using the Mizar system [1], we define the Gauge integral (Henstock-Kurzweil) of a real-valued function on a real interval [a, b] (see [2], [3], [15], [14], [11]). In the next section we formalize that the Henstock-Kurzweil integral is linear. In the last section, we verified that a real-valued bounded integrable (in sense Darboux/Riemann [6, 7, 8]) function over a interval a, b is Gauge integrable. Note that, in accordance with the possibilities of the MML [9], we reuse a large part of demonstrations already present in another article. Instead of rewriting the proof already contained in [7] (MML Version: 5.42.1290), we slightly modified this article in order to use directly the expected results.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
Using the Mizar system [2], we formalized that homographies of the projective real plane (as defined in [5]), form a group. Then, we prove that, using the notations of Borsuk and Szmielew in [3] “Consider in space ℝℙ2 points P1, P2, P3, P4 of which three points are not collinear and points Q1,Q2,Q3,Q4 each three points of which are also not collinear. There exists one homography h of space ℝℙ2 such that h(Pi) = Qi for i = 1, 2, 3, 4.” (Existence Statement 52 and Existence Statement 53) [3]. Or, using notations of Richter [11] “Let [a], [b], [c], [d] in ℝℙ2 be four points of which no three are collinear and let [a′],[b′],[c′],[d′] in ℝℙ2 be another four points of which no three are collinear, then there exists a 3 × 3 matrix M such that [Ma] = [a′], [Mb] = [b′], [Mc] = [c′], and [Md] = [d′]” Makarios has formalized the same results in Isabelle/Isar (the collineations form a group, lemma statement52-existence and lemma statement 53-existence) and published it in Archive of Formal Proofs [10], [9].
3
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article we check, with the Mizar system [2], Pascal’s theorem in the real projective plane (in projective geometry Pascal’s theorem is also known as the Hexagrammum Mysticum Theorem)1. Pappus’ theorem is a special case of a degenerate conic of two lines. For proving Pascal’s theorem, we use the techniques developed in the section “Projective Proofs of Pappus’ Theorem” in the chapter “Pappus’ Theorem: Nine proofs and three variations” [11]. We also follow some ideas from Harrison’s work. With HOL Light, he has the proof of Pascal’s theorem2. For a lemma, we use PROVER93 and OTT2MIZ by Josef Urban4 [12, 6, 7]. We note, that we don’t use Skolem/Herbrand functions (see “Skolemization” in [1]).
4
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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.” (In the plane YOX let S be a connected area bounded by a closed contour, simple or complex; one supposes that at each point of S or its perimeter there is a circle, of non-zero radius, having this point as its centre; it is then always possible to subdivide S into regions, finite in number and sufficiently small for each one of them to be entirely inside a circle corresponding to a suitably chosen point in S or on its perimeter) [23]. 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].
5
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
Schmets [22] has developed a measure theory from a generalized notion of a semiring of sets. Goguadze [15] has introduced another generalized notion of semiring of sets and proved that all known properties that semiring have according to the old definitions are preserved. We show that this two notions are almost equivalent. We note that Patriota [20] has defined this quasi-semiring. We propose the formalization of some properties developed by the authors.
6
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
We introduce the altitudes of a triangle (the cevians perpendicular to the opposite sides). Using the generalized Ceva’s Theorem, we prove the existence and uniqueness of the orthocenter of a triangle [7]. Finally, we formalize in Mizar [1] some formulas [2] to calculate distance using triangulation.
7
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article, using mostly Pervin [9], Kunzi [6], [8], [7], Williams [11] and Bourbaki [3] works, we formalize in Mizar [2] the notions of quasiuniform space, semi-uniform space and locally uniform space. We define the topology induced by a quasi-uniform space. Finally we formalize from the sets of the form ((X \ Ω) × X) ∪ (X × Ω), the Csaszar-Pervin quasi-uniform space induced by a topological space.
8
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article, we formalize in Mizar [1] the notion of uniform space introduced by André Weil using the concepts of entourages [2]. We present some results between uniform space and pseudo metric space. We introduce the concepts of left-uniformity and right-uniformity of a topological group. Next, we define the concept of the partition topology. Following the Vlach’s works [11, 10], we define the semi-uniform space induced by a tolerance and the uniform space induced by an equivalence relation. Finally, using mostly Gehrke, Grigorieff and Pin [4] works, a Pervin uniform space defined from the sets of the form ((X\A) × (X\A)) ∪ (A×A) is presented.
9
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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 ℝn [16], semi-intervalle (borné) de ℝn [22]). We conclude with the definition of Chebyshev distance [11].
10
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
We introduce, using the Mizar system [1], some basic concepts of Euclidean geometry: the half length and the midpoint of a segment, the perpendicular bisector of a segment, the medians (the cevians that join the vertices of a triangle to the midpoints of the opposite sides) of a triangle. We prove the existence and uniqueness of the circumcenter of a triangle (the intersection of the three perpendicular bisectors of the sides of the triangle). The extended law of sines and the formula of the radius of the Morley’s trisector triangle are formalized [3]. Using the generalized Ceva’s Theorem, we prove the existence and uniqueness of the centroid (the common point of the medians [4]) of a triangle.
11
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
We calculate the values of the trigonometric functions for angles: [XXX] , by [16]. After defining some trigonometric identities, we demonstrate conventional trigonometric formulas in the triangle, and the geometric property, by [14], of the triangle inscribed in a semicircle, by the proposition 3.31 in [15]. Then we define the diameter of the circumscribed circle of a triangle using the definition of the area of a triangle and prove some identities of a triangle [9]. We conclude by indicating that the diameter of a circle is twice the length of the radius
12
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
First, we define in Mizar [5], the Cartesian product of two filters bases and the Cartesian product of two filters. After comparing the product of two Fréchet filters on ℕ (F1) with the Fréchet filter on ℕ × ℕ (F2), we compare limF₁ and limF₂ for all double sequences in a non empty topological space. Endou, Okazaki and Shidama formalized in [14] the “convergence in Pringsheim’s sense” for double sequence of real numbers. We show some basic correspondences between the p-convergence and the filter convergence in a topological space. Then we formalize that the double sequence [...] converges in “Pringsheim’s sense” but not in Frechet filter on ℕ × ℕ sense. In the next section, we generalize some definitions: “is convergent in the first coordinate”, “is convergent in the second coordinate”, “the lim in the first coordinate of”, “the lim in the second coordinate of” according to [14], in Hausdorff space. Finally, we generalize two theorems: (3) and (4) from [14] in the case of double sequences and we formalize the “iterated limit” theorem (“Double limit” [7], p. 81, par. 8.5 “Double limite” [6] (TG I,57)), all in regular space. We were inspired by the exercises (2.11.4), (2.17.5) [17] and the corrections B.10 [18].
13
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
The real projective plane has been formalized in Isabelle/HOL by Timothy Makarios [13] and in Coq by Nicolas Magaud, Julien Narboux and Pascal Schreck [12]. Some definitions on the real projective spaces were introduced early in the Mizar Mathematical Library by Wojciech Leonczuk [9], Krzysztof Prazmowski [10] and by Wojciech Skaba [18]. In this article, we check with the Mizar system [4], some properties on the determinants and the Grassmann-Plücker relation in rank 3 [2], [1], [7], [16], [17]. Then we show that the projective space induced (in the sense defined in [9]) by ℝ3 is a projective plane (in the sense defined in [10]). Finally, in the real projective plane, we define the homography induced by a 3-by-3 invertible matrix and we show that the images of 3 collinear points are themselves collinear.
15
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
We are inspired by the work of Henri Cartan [16], Bourbaki [10] (TG. I Filtres) and Claude Wagschal [34]. We define the base of filter, image filter, convergent filter bases, limit filter and the filter base of tails (fr: filtre des sections).
16
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
Hölzl et al. showed that it was possible to build “a generic theory of limits based on filters” in Isabelle/HOL [22], [7]. In this paper we present our formalization of this theory in Mizar [6]. First, we compare the notions of the limit of a family indexed by a directed set, or a sequence, in a metric space [30], a real normed linear space [29] and a linear topological space [14] with the concept of the limit of an image filter [16]. Then, following Bourbaki [9], [10] (TG.III, §5.1 Familles sommables dans un groupe commutatif), we conclude by defining the summable families in a commutative group (“additive notation” in [17]), using the notion of filters.
17
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
Using Mizar [9], and the formal topological space structure (FMT_Space_Str) [19], we introduce the three U-FMT conditions (U-FMT filter, U-FMT with point and U-FMT local) similar to those VI, VII, VIII and VIV of the proposition 2 in [10]: If to each element x of a set X there corresponds a set B(x) of subsets of X such that the properties VI, VII, VIII and VIV are satisfied, then there is a unique topological structure on X such that, for each x ∈ X, B(x) is the set of neighborhoods of x in this topology. We present a correspondence between a topological space and a space defined with the formal topological space structure with the three U-FMT conditions called the topology from neighbourhoods. For the formalization, we were inspired by the works of Bourbaki [11] and Claude Wagschal [31].
18
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
We formalize that the image of a semiring of sets [17] by an injective function is a semiring of sets.We offer a non-trivial example of a semiring of sets in a topological space [21]. Finally, we show that the finite product of a semiring of sets is also a semiring of sets [21] and that the finite product of a classical semiring of sets [8] is a classical semiring of sets. In this case, we use here the notation from the book of Aliprantis and Border [1].
19
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
We translate the articles covering group theory already available in the Mizar Mathematical Library from multiplicative into additive notation. We adapt the works of Wojciech A. Trybulec [41, 42, 43] and Artur Korniłowicz [25]. In particular, these authors have defined the notions of group, abelian group, power of an element of a group, order of a group and order of an element, subgroup, coset of a subgroup, index of a subgroup, conjugation, normal subgroup, topological group, dense subset and basis of a topological group. Lagrange’s theorem and some other theorems concerning these notions [9, 24, 22] are presented. Note that “The term ℤ-module is simply another name for an additive abelian group” [27]. We take an approach different than that used by Futa et al. [21] to use in a future article the results obtained by Artur Korniłowicz [25]. Indeed, Hölzl et al. showed that it was possible to build “a generic theory of limits based on filters” in Isabelle/HOL [23, 10]. Our goal is to define the convergence of a sequence and the convergence of a series in an abelian topological group [11] using the notion of filters.
20
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
Morley’s trisector theorem states that “The points of intersection of the adjacent trisectors of the angles of any triangle are the vertices of an equilateral triangle” [10]. There are many proofs of Morley’s trisector theorem [12, 16, 9, 13, 8, 20, 3, 18]. We follow the proof given by A. Letac in [15].
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.