rss_2.0Formalized Mathematics FeedSciendo RSS Feed for Formalized Mathematicshttps://sciendo.com/journal/FORMAhttps://www.sciendo.comFormalized Mathematics 's Coverhttps://sciendo-parsed-data-feed.s3.eu-central-1.amazonaws.com/60a83a16afabd64053833755/cover-image.jpg?X-Amz-Algorithm=AWS4-HMAC-SHA256&X-Amz-Date=20220627T200335Z&X-Amz-SignedHeaders=host&X-Amz-Expires=604800&X-Amz-Credential=AKIA6AP2G7AKP25APDM2%2F20220627%2Feu-central-1%2Fs3%2Faws4_request&X-Amz-Signature=a7b0ac2b22804fb3ed257d1f12cfee9407a00961e3be4c3a5d9f1486f4d2af6a200300Algorithm NextFit for the Bin Packing Problemhttps://sciendo.com/article/10.2478/forma-2021-0014<abstract> <p><bold>Summary</bold>. The bin packing problem is a fundamental and important optimization problem in theoretical computer science [4], [6]. An instance is a sequence of items, each being of positive size at most one. The task is to place all the items into bins so that the total size of items in each bin is at most one and the number of bins that contain at least one item is minimum.</p> <p>Approximation algorithms have been intensively studied. Algorithm NextFit would be the simplest one. The algorithm repeatedly does the following: If the first unprocessed item in the sequence can be placed, in terms of size, additionally to the bin into which the algorithm has placed an item the last time, place the item into that bin; otherwise place the item into an empty bin. Johnson [5] proved that the number of the resulting bins by algorithm NextFit is less than twice the number of the fewest bins that are needed to contain all items.</p> <p>In this article, we formalize in Mizar [1], [2] the bin packing problem as follows: An instance is a sequence of positive real numbers that are each at most one. The task is to find a function that maps the indices of the sequence to positive integers such that the sum of the subsequence for each of the inverse images is at most one and the size of the image is minimum. We then formalize algorithm NextFit, its feasibility, its approximation guarantee, and the tightness of the approximation guarantee.</p> </abstract>ARTICLE2021-12-30T00:00:00.000+00:00Real Vector Space and Related Notionshttps://sciendo.com/article/10.2478/forma-2021-0012<abstract> <p><bold>Summary</bold>. In this paper, we discuss the properties that hold in finite dimensional vector spaces and related spaces. In the Mizar language [1], [2], variables are strictly typed, and their type conversion requires a complicated process. Our purpose is to formalize that some properties of finite dimensional vector spaces are preserved in type transformations, and to contain the complexity of type transformations into this paper. Specifically, we show that properties such as algebraic structure, subsets, finite sequences and their sums, linear combination, linear independence, and affine independence are preserved in type conversions among <monospace>TOP-REAL(n)</monospace>, <monospace>REAL-NS(n)</monospace>, and <monospace>n-VectSp over F Real</monospace>. We referred to [4], [9], and [8] in the formalization.</p> </abstract>ARTICLE2021-12-30T00:00:00.000+00:00Splitting Fieldshttps://sciendo.com/article/10.2478/forma-2021-0013<abstract> <p><bold>Summary</bold>. In this article we further develop field theory in Mizar [1], [2]: we prove existence and uniqueness of splitting fields. We define the splitting field of a polynomial <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>] as the smallest field extension of <italic>F</italic>, in which <italic>p</italic> splits into linear factors. From this follows, that for a splitting field <italic>E</italic> of <italic>p</italic> we have <italic>E</italic> = <italic>F</italic> (<italic>A</italic>) where <italic>A</italic> is the set of <italic>p</italic>’s roots. Splitting fields are unique, however, only up to isomorphisms; to be more precise up to <italic>F</italic> -isomorphims i.e. isomorphisms <italic>i</italic> with <italic>i|<sub>F</sub></italic> = Id<italic><sub>F</sub></italic>. We prove that two splitting fields of <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>] are <italic>F</italic> -isomorphic using the well-known technique [4], [3] of extending isomorphisms from <italic>F</italic><sub>1</sub> → <italic>F</italic><sub>2</sub> to <italic>F</italic><sub>1</sub>(<italic>a</italic>) → <italic>F</italic><sub>2</sub>(<italic>b</italic>) for <italic>a</italic> and <italic>b</italic> being algebraic over <italic>F</italic><sub>1</sub> and <italic>F</italic><sub>2</sub>, respectively.</p> </abstract>ARTICLE2021-12-30T00:00:00.000+00:00Some Properties of Membership Functions Composed of Triangle Functions and Piecewise Linear Functionshttps://sciendo.com/article/10.2478/forma-2021-0011<abstract> <p><bold>Summary</bold>. IF-THEN rules in fuzzy inference is composed of multiple fuzzy sets (membership functions). IF-THEN rules can therefore be considered as a pair of membership functions [7]. The evaluation function of fuzzy control is composite function with fuzzy approximate reasoning and is functional on the set of membership functions. We obtained continuity of the evaluation function and compactness of the set of membership functions [12]. Therefore, we proved the existence of pair of membership functions, which maximizes (minimizes) evaluation function and is considered IF-THEN rules, in the set of membership functions by using extreme value theorem. The set of membership functions (fuzzy sets) is defined in this article to verifier our proofs before by Mizar [9], [10], [4]. Membership functions composed of triangle function, piecewise linear function and Gaussian function used in practice are formalized using existing functions.</p> <p>On the other hand, not only curve membership functions mentioned above but also membership functions composed of straight lines (piecewise linear function) like triangular and trapezoidal functions are formalized. Moreover, different from the definition in [3] formalizations of triangular and trapezoidal function composed of two straight lines, minimum function and maximum functions are proposed. We prove, using the Mizar [2], [1] formalism, some properties of membership functions such as continuity and periodicity [13], [8].</p> </abstract>ARTICLE2021-12-30T00:00:00.000+00:00On Primary Ideals. Part Ihttps://sciendo.com/article/10.2478/forma-2021-0010<abstract> <p><bold>Summary</bold>. We formalize in the Mizar System [3], [4], definitions and basic propositions about primary ideals of a commutative ring along with Chapter 4 of [1] and Chapter III of [8]. Additionally other necessary basic ideal operations such as compatibilities taking radical and intersection of finite number of ideals are formalized as well in order to prove theorems relating primary ideals. These basic operations are mainly quoted from Chapter 1 of [1] and compiled as preliminaries in the first half of the article.</p> </abstract>ARTICLE2021-12-30T00:00:00.000+00:00Ascoli-Arzelà Theoremhttps://sciendo.com/article/10.2478/forma-2021-0009<abstract> <p><bold>Summary</bold>. In this article we formalize the Ascoli-Arzelà theorem [5], [6], [8] in Mizar [1], [2]. First, we gave definitions of equicontinuousness and equiboundedness of a set of continuous functions [12], [7], [3], [9]. Next, we formalized the Ascoli-Arzelà theorem using those definitions, and proved this theorem.</p> </abstract>ARTICLE2021-12-30T00:00:00.000+00:00On Weakly Associative Lattices and Near Latticeshttps://sciendo.com/article/10.2478/forma-2021-0008<abstract> <p><bold>Summary</bold>. The main aim of this article is to introduce formally two generalizations of lattices, namely weakly associative lattices and near lattices, which can be obtained from the former by certain weakening of the usual well-known axioms. We show selected propositions devoted to weakly associative lattices and near lattices from Chapter 6 of [15], dealing also with alternative versions of classical axiomatizations. Some of the results were proven in the Mizar [1], [2] system with the help of Prover9 [14] proof assistant.</p> </abstract>ARTICLE2021-12-30T00:00:00.000+00:00Pappus’s Hexagon Theorem in Real Projective Planehttps://sciendo.com/article/10.2478/forma-2021-0007<abstract> <p><bold>Summary</bold>. In this article we prove, using Mizar [2], [1], the Pappus’s hexagon theorem in the real projective plane: “Given one set of collinear points <italic>A, B, C</italic>, and another set of collinear points <italic>a, b, c</italic>, then the intersection points <italic>X, Y, Z</italic> of line pairs <italic>Ab</italic> and <italic>aB, Ac</italic> and <italic>aC, Bc</italic> and <italic>bC</italic> are collinear”<fn id="j_forma-2021-0007_fn_2" symbol="2"><p><ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://en.wikipedia.org/wiki/Pappus’s_hexagon_theorem">https://en.wikipedia.org/wiki/Pappus’s_hexagon_theorem</ext-link></p></fn>.</p> <p>More precisely, we prove that the structure <monospace>ProjectiveSpace TOP-REAL3</monospace> [10] (where <monospace>TOP-REAL3</monospace> is a metric space defined in [5]) satisfies the Pappus’s axiom defined in [11] by Wojciech Leończuk and Krzysztof Prażmowski. Eugeniusz Kusak and Wojciech Leończuk formalized the Hessenberg theorem early in the MML [9]. With this result, the real projective plane is Desarguesian. For proving the Pappus’s theorem, two different proofs are given. First, we use the techniques developed in the section “Projective Proofs of Pappus’s Theorem” in the chapter “Pappos’s Theorem: Nine proofs and three variations” [12]. Secondly, Pascal’s theorem [4] is used.</p> <p>In both cases, to prove some lemmas, we use <monospace>Prover9</monospace><fn id="j_forma-2021-0007_fn_3" symbol="3"><p><ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://www.cs.unm.edu/~mccune/prover9/">https://www.cs.unm.edu/~mccune/prover9/</ext-link></p></fn>, the successor of the <monospace>Otter</monospace> prover and <monospace>ott2miz</monospace> by Josef Urban<fn id="j_forma-2021-0007_fn_4" symbol="4"><p>See its homepage <ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://github.com/JUrban/ott2miz">https://github.com/JUrban/ott2miz</ext-link></p></fn> [13], [8], [7].</p> <p>In <monospace>Coq</monospace>, the Pappus’s theorem is proved as the application of Grassmann-Cayley algebra [6] and more recently in Tarski’s geometry [3].</p> </abstract>ARTICLE2021-12-30T00:00:00.000+00:00Functional Sequence in Norm Spacehttps://sciendo.com/article/10.2478/forma-2020-0023<abstract> <title style='display:none'>Summary</title> <p>In this article, we formalize in Mizar [1], [2] functional sequences and basic operations on functional sequences in norm space based on [5]. In the first section, we define functional sequence in norm space. In the second section, we define pointwise convergence and prove some related theorems. In the last section we define uniform convergence and limit of functional sequence.</p> </abstract>ARTICLE2021-05-21T00:00:00.000+00:00Partial Correctness of an Algorithm Computing Lucas Sequenceshttps://sciendo.com/article/10.2478/forma-2020-0025<abstract> <title style='display:none'>Summary</title> <p>In this paper we define some properties about finite sequences and verify the partial correctness of an algorithm computing <italic>n</italic>-th element of Lucas sequence [23], [20] with given <italic>P</italic> and <italic>Q</italic> coefficients as well as two first elements (<italic>x</italic> and <italic>y</italic>). The algorithm is encoded in nominative data language [22] in the Mizar system [3], [1].</p> <p><disp-quote><p><monospace>i := 0</monospace></p> <p><monospace>s := x</monospace></p> <p><monospace>b := y</monospace></p> <p><monospace>c := x</monospace></p> <p><monospace>while (i &lt;&gt; n)</monospace></p> <p> <monospace>c := s</monospace></p> <p> <monospace>s := b</monospace></p> <p> <monospace>ps := p*s</monospace></p> <p> <monospace>qc := q*c</monospace></p> <p> <monospace>b := ps − qc</monospace></p> <p> <monospace>i := i + j</monospace></p> <p><monospace>return s</monospace></p></disp-quote></p> <p>This paper continues verification of algorithms [10], [14], [12], [15], [13] written in terms of simple-named complex-valued nominative data [6], [8], [19], [11], [16], [17]. The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2], [4] with partial pre- and post-conditions [18], [21], [7], [5].</p> </abstract>ARTICLE2021-05-21T00:00:00.000+00:00General Theory and Tools for Proving Algorithms in Nominative Data Systemshttps://sciendo.com/article/10.2478/forma-2020-0024<abstract> <title style='display:none'>Summary</title> <p>In this paper we introduce some new definitions for sequences of operations and extract general theorems about properties of iterative algorithms encoded in nominative data language [20] in the Mizar system [3], [1] in order to simplify the process of proving algorithms in the future.</p> <p>This paper continues verification of algorithms [10], [13], [12], [14] written in terms of simple-named complex-valued nominative data [6], [8], [18], [11], [15], [16].</p> <p>The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2], [4] with partial pre- and postconditions [17], [19], [7], [5].</p> </abstract>ARTICLE2021-05-21T00:00:00.000+00:00Functional Space Consisted by Continuous Functions on Topological Spacehttps://sciendo.com/article/10.2478/forma-2021-0005<abstract> <title style='display:none'>Summary</title> <p>In this article, using the Mizar system [1], [2], first we give a definition of a functional space which is constructed from all continuous functions defined on a compact topological space [5]. We prove that this functional space is a Banach space [3]. Next, we give a definition of a function space which is constructed from all continuous functions with bounded support. We also prove that this function space is a normed space.</p> </abstract>ARTICLE2021-08-26T00:00:00.000+00:00Inverse Function Theorem. Part Ihttps://sciendo.com/article/10.2478/forma-2021-0002<abstract> <title style='display:none'>Summary</title> <p>In this article we formalize in Mizar [1], [2] the inverse function theorem for the class of <italic>C</italic><sup>1</sup> functions between Banach spaces. In the first section, we prove several theorems about open sets in real norm space, which are needed in the proof of the inverse function theorem. In the next section, we define a function to exchange the order of a product of two normed spaces, namely 𝔼 ↶ ≂ (<italic>x, y</italic>) ∈ <italic>X × Y</italic> ↦ (<italic>y, x</italic>) ∈ <italic>Y × X</italic>, and formalized its bijective isometric property and several differentiation properties. This map is necessary to change the order of the arguments of a function when deriving the inverse function theorem from the implicit function theorem proved in [6].</p> <p>In the third section, using the implicit function theorem, we prove a theorem that is a necessary component of the proof of the inverse function theorem. In the last section, we finally formalized an inverse function theorem for class of <italic>C</italic><sup>1</sup> functions between Banach spaces. We referred to [9], [10], and [3] in the formalization.</p> </abstract>ARTICLE2021-08-26T00:00:00.000+00:00Elementary Number Theory Problems. Part IIhttps://sciendo.com/article/10.2478/forma-2021-0006<abstract> <title style='display:none'>Summary</title> <p>In this paper problems 14, 15, 29, 30, 34, 78, 83, 97, and 116 from [6] are formalized, using the Mizar formalism [1], [2], [3]. Some properties related to the divisibility of prime numbers were proved. It has been shown that the equation of the form <italic>p</italic><sup>2</sup> + 1 = <italic>q</italic><sup>2</sup> + <italic>r</italic><sup>2</sup>, where <italic>p</italic>, <italic>q</italic>, <italic>r</italic> are prime numbers, has at least four solutions and it has been proved that at least five primes can be represented as the sum of two fourth powers of integers. We also proved that for at least one positive integer, the sum of the fourth powers of this number and its successor is a composite number. And finally, it has been shown that there are infinitely many odd numbers <italic>k</italic> greater than zero such that all numbers of the form 2<sup>2</sup><italic><sup>n</sup></italic> + <italic>k</italic> (<italic>n</italic> = 1, 2, . . . ) are composite.</p> </abstract>ARTICLE2021-08-26T00:00:00.000+00:00Miscellaneous Graph Preliminaries. Part Ihttps://sciendo.com/article/10.2478/forma-2021-0003<abstract> <title style='display:none'>Summary</title> <p>This article contains many auxiliary theorems which were missing in the Mizar Mathematical Library to the best of the author’s knowledge. Most of them regard graph theory as formalized in the GLIB series and are needed in upcoming articles.</p> </abstract>ARTICLE2021-08-26T00:00:00.000+00:00Derivation of Commutative Rings and the Leibniz Formula for Power of Derivationhttps://sciendo.com/article/10.2478/forma-2021-0001<abstract> <title style='display:none'>Summary</title> <p>In this article we formalize in Mizar [1], [2] a derivation of commutative rings, its definition and some properties. The details are to be referred to [5], [7]. A derivation of a ring, say <italic>D</italic>, is defined generally as a map from a commutative ring <italic>A</italic> to <italic>A</italic>-Module <italic>M</italic> with specific conditions. However we start with simpler case, namely dom <italic>D</italic> = rng <italic>D</italic>. This allows to define a derivation in other rings such as a polynomial ring.</p> <p>A derivation is a map <italic>D</italic> : <italic>A → A</italic> satisfying the following conditions:</p> <p>(i) <italic>D</italic>(<italic>x</italic> + <italic>y</italic>) = <italic>Dx</italic> + <italic>Dy</italic>,</p> <p>(ii) <italic>D</italic>(<italic>xy</italic>) = <italic>xDy</italic> + <italic>yDx</italic>, ∀<italic>x, y</italic> ∈ <italic>A</italic>.</p> <p>Typical properties are formalized such as: <disp-formula> <alternatives> <graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2021-0001_eq_001.png"/> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mml:mrow><mml:mi>D</mml:mi><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:munderover><mml:mo>∑</mml:mo><mml:mrow><mml:mi>i</mml:mi><mml:mo>=</mml:mo><mml:mn>1</mml:mn></mml:mrow><mml:mi>n</mml:mi></mml:munderover><mml:mrow><mml:msub><mml:mrow><mml:mi>x</mml:mi></mml:mrow><mml:mi>i</mml:mi></mml:msub></mml:mrow></mml:mrow><mml:mo>)</mml:mo></mml:mrow><mml:mo>=</mml:mo><mml:munderover><mml:mo>∑</mml:mo><mml:mrow><mml:mi>i</mml:mi><mml:mo>=</mml:mo><mml:mn>1</mml:mn></mml:mrow><mml:mi>n</mml:mi></mml:munderover><mml:mrow><mml:mi>D</mml:mi><mml:msub><mml:mrow><mml:mi>x</mml:mi></mml:mrow><mml:mi>i</mml:mi></mml:msub></mml:mrow></mml:mrow></mml:math> <tex-math>D\left( {\sum\limits_{i = 1}^n {{x_i}} } \right) = \sum\limits_{i = 1}^n {D{x_i}}</tex-math> </alternatives> </disp-formula> and <disp-formula> <alternatives> <graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2021-0001_eq_002.png"/> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mml:mrow><mml:mi>D</mml:mi><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:munderover><mml:mo>∏</mml:mo><mml:mrow><mml:mi>i</mml:mi><mml:mo>=</mml:mo><mml:mn>1</mml:mn></mml:mrow><mml:mi>n</mml:mi></mml:munderover><mml:mrow><mml:msub><mml:mrow><mml:mi>x</mml:mi></mml:mrow><mml:mi>i</mml:mi></mml:msub></mml:mrow></mml:mrow><mml:mo>)</mml:mo></mml:mrow><mml:mo>=</mml:mo><mml:munderover><mml:mo>∑</mml:mo><mml:mrow><mml:mi>i</mml:mi><mml:mo>=</mml:mo><mml:mn>1</mml:mn></mml:mrow><mml:mi>n</mml:mi></mml:munderover><mml:mrow><mml:msub><mml:mrow><mml:mi>x</mml:mi></mml:mrow><mml:mn>1</mml:mn></mml:msub><mml:msub><mml:mrow><mml:mi>x</mml:mi></mml:mrow><mml:mn>2</mml:mn></mml:msub><mml:mo>⋯</mml:mo><mml:mi>D</mml:mi><mml:msub><mml:mrow><mml:mi>x</mml:mi></mml:mrow><mml:mi>i</mml:mi></mml:msub><mml:mo>⋯</mml:mo><mml:msub><mml:mrow><mml:mi>x</mml:mi></mml:mrow><mml:mi>n</mml:mi></mml:msub></mml:mrow><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:mo>∀</mml:mo><mml:msub><mml:mrow><mml:mi>x</mml:mi></mml:mrow><mml:mi>i</mml:mi></mml:msub><mml:mo>∈</mml:mo><mml:mi>A</mml:mi></mml:mrow><mml:mo>)</mml:mo></mml:mrow><mml:mo>.</mml:mo></mml:mrow></mml:math> <tex-math>D\left( {\prod\limits_{i = 1}^n {{x_i}} } \right) = \sum\limits_{i = 1}^n {{x_1}{x_2} \cdots D{x_i} \cdots {x_n}} \left( {\forall {x_i} \in A} \right).</tex-math> </alternatives> </disp-formula></p> <p>We also formalized the Leibniz Formula for power of derivation <italic>D</italic> : <disp-formula> <alternatives> <graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2021-0001_eq_003.png"/> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mml:mrow><mml:msup><mml:mrow><mml:mi>D</mml:mi></mml:mrow><mml:mi>n</mml:mi></mml:msup><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:mi>x</mml:mi><mml:mi>y</mml:mi></mml:mrow><mml:mo>)</mml:mo></mml:mrow><mml:mo>=</mml:mo><mml:munderover><mml:mo>∑</mml:mo><mml:mrow><mml:mi>i</mml:mi><mml:mo>=</mml:mo><mml:mn>0</mml:mn></mml:mrow><mml:mi>n</mml:mi></mml:munderover><mml:mrow><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:msubsup><mml:mrow/><mml:mi>i</mml:mi><mml:mi>n</mml:mi></mml:msubsup></mml:mrow><mml:mo>)</mml:mo></mml:mrow><mml:msup><mml:mrow><mml:mi>D</mml:mi></mml:mrow><mml:mi>i</mml:mi></mml:msup><mml:mi>x</mml:mi><mml:msup><mml:mrow><mml:mi>D</mml:mi></mml:mrow><mml:mrow><mml:mi>n</mml:mi><mml:mo>-</mml:mo><mml:mi>i</mml:mi></mml:mrow></mml:msup><mml:mi>y</mml:mi><mml:mo>.</mml:mo></mml:mrow></mml:mrow></mml:math> <tex-math>{D^n}\left( {xy} \right) = \sum\limits_{i = 0}^n {\left( {_i^n} \right){D^i}x{D^{n - i}}y.}</tex-math> </alternatives> </disp-formula></p> <p>Lastly applying the definition to the polynomial ring of <italic>A</italic> and a derivation of polynomial ring was formalized. We mentioned a justification about compatibility of the derivation in this article to the same object that has treated as differentiations of polynomial functions [3].</p> </abstract>ARTICLE2021-08-26T00:00:00.000+00:00Algebraic Extensionshttps://sciendo.com/article/10.2478/forma-2021-0004<abstract> <title style='display:none'>Summary</title> <p>In this article we further develop field theory in Mizar [1], [2], [3] towards splitting fields. We deal with algebraic extensions [4], [5]: a field extension <italic>E</italic> of a field <italic>F</italic> is algebraic, if every element of <italic>E</italic> is algebraic over <italic>F</italic>. We prove amongst others that finite extensions are algebraic and that field extensions generated by a finite set of algebraic elements are finite. From this immediately follows that field extensions generated by roots of a polynomial over <italic>F</italic> are both finite and algebraic. We also define the field of algebraic elements of <italic>E</italic> over <italic>F</italic> and show that this field is an intermediate field of <italic>E|F.</italic></p> </abstract>ARTICLE2021-08-26T00:00:00.000+00:00A Case Study of Transporting Urysohn’s Lemma from Topology via Open Sets into Topology via Neighborhoodshttps://sciendo.com/article/10.2478/forma-2020-0020<abstract><title style='display:none'>Summary</title><p>Józef Białas and Yatsuka Nakamura has completely formalized a proof of Urysohn’s lemma in the article [4], in the context of a topological space defined via open sets. In the Mizar Mathematical Library (MML), the topological space is defined in this way by Beata Padlewska and Agata Darmochwał in the article [18]. In [7] the topological space is defined via neighborhoods. It is well known that these definitions are equivalent [5, 6].</p><p>In the definitions, an abstract structure (i.e. the article [17, STRUCT 0] and its descendants, all of them directly or indirectly using Mizar structures [3]) have been used (see [10], [9]). The first topological definition is based on the Mizar structure TopStruct and the topological space defined via neighborhoods with the Mizar structure: FMT Space Str. To emphasize the notion of a neighborhood, we rename FMT TopSpace (topology from neighbourhoods) to NTopSpace (a neighborhood topological space).</p><p>Using Mizar [2], we transport the Urysohn’s lemma from TopSpace to NTop-Space.</p><p>In some cases, Mizar allows certain techniques for transporting proofs, definitions or theorems. Generally speaking, there is no such automatic translating.</p><p>In Coq, Isabelle/HOL or homotopy type theory transport is also studied, sometimes with a more systematic aim [14], [21], [11], [12], [8], [19]. In [1], two co-existing Isabelle libraries: Isabelle/HOL and Isabelle/Mizar, have been aligned in a single foundation in the Isabelle logical framework.</p><p>In the MML, they have been used since the beginning: reconsider, registration, cluster, others were later implemented [13]: identify.</p><p>In some proofs, it is possible to define particular functors between different structures, mainly useful when results are already obtained in a given structure. This technique is used, for example, in [15] to define two functors MXR2MXF and MXF2MXF between Matrix of REAL and Matrix of F-Real and to transport the definition of the addition from one structure to the other: [...] A + B -&gt; Matrix of REAL equals MXF2MXR ((MXR2MXF A) + (MXR2MXF B)) [...].</p><p>In this paper, first we align the necessary topological concepts. For the formalization, we were inspired by the works of Claude Wagschal [20]. It allows us to transport more naturally the Urysohn’s lemma ([4, URYSOHN3:20]) to the topological space defined via neighborhoods.</p><p>Nakasho and Shidama have developed a solution to explore the notions introduced in various ways <ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://mimosa-project.github.io/mmlreference/current/">https://mimosa-project.github.io/mmlreference/current/</ext-link> [16].</p><p>The definitions can be directly linked in the HTML version of the Mizar library (example: Urysohn’s lemma <ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="http://mizar.org/version/current/html/urysohn3.html#T20">http://mizar.org/version/current/html/urysohn3.html#T20</ext-link>).</p></abstract>ARTICLE2021-04-06T00:00:00.000+00:00Extended Natural Numbers and Countershttps://sciendo.com/article/10.2478/forma-2020-0021<abstract><title style='display:none'>Summary</title><p>This article introduces extended natural numbers, i.e. the set ℕ ∪ {+∞}, in Mizar [4], [3] and formalizes a way to list a cardinal numbers of cardinals. Both concepts have applications in graph theory.</p></abstract>ARTICLE2021-04-06T00:00:00.000+00:00Ring and Field Adjunctions, Algebraic Elements and Minimal Polynomialshttps://sciendo.com/article/10.2478/forma-2020-0022<abstract><title style='display:none'>Summary</title><p>In [6], [7] we presented a formalization of Kronecker’s construction of a field extension of a field <italic>F</italic> in which a given polynomial <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]<italic>\F</italic> has a root [4], [5], [3]. As a consequence for every field <italic>F</italic> and every polynomial there exists a field extension <italic>E</italic> of <italic>F</italic> in which <italic>p</italic> splits into linear factors. It is well-known that one gets the smallest such field extension – the splitting field of <italic>p</italic> – by adjoining the roots of <italic>p</italic> to <italic>F</italic>.</p><p>In this article we start the Mizar formalization [1], [2] towards splitting fields: we define ring and field adjunctions, algebraic elements and minimal polynomials and prove a number of facts necessary to develop the theory of splitting fields, in particular that for an algebraic element <italic>a</italic> over <italic>F</italic> a basis of the vector space <italic>F</italic> (<italic>a</italic>) over <italic>F</italic> is given by <italic>a</italic><sup>0</sup><italic>, . . ., a<sup>n−</sup></italic><sup>1</sup>, where <italic>n</italic> is the degree of the minimal polynomial of <italic>a</italic> over <italic>F</italic> .</p></abstract>ARTICLE2021-04-06T00:00:00.000+00:00en-us-1