http://hdl.handle.net/11320/15399 2026-06-01T16:21:04Z http://hdl.handle.net/11320/15867 Tytuł: Extensions of Orderings Autorzy: Schwarzweller, Christoph Abstrakt: In this article we extend the algebraic theory of ordered fields [6], [8] in Mizar. We introduce extensions of orderings: if E is a field extension of F, then an ordering P of F extends to E, if there exists an ordering O of E containing P. We first prove some necessary and sufficient conditions for P being extendable to E, in particular that P extends to E if and only if the set QS E := {∑a ∗ b²| a ∈ P, b ∈ E} is a preordering of E – or equivalently if and only if −1 ∈/ QS E. Then we show for non-square a ∈ F that P extends to F(√a) if and only if P and finally that every ordering P of F extends to E if the degree of E over F is odd. 2023-01-01T00:00:00Z http://hdl.handle.net/11320/15866 Tytuł: Tarski Geometry Axioms. Part V – Half-planes and Planes Autorzy: Coghetto, Roland; Grabowski, Adam Abstrakt: In the article, we continue the formalization of the work devoted to Tarski’s geometry – the book “Metamathematische Methoden in der Geometrie” by W. Schwabhäuser, W. Szmielew, and A. Tarski. We use the Mizar system to formalize Chapter 9 of this book. We deal with half-planes and planes proving their properties as well as the theory of intersecting lines. 2023-01-01T00:00:00Z http://hdl.handle.net/11320/15864 Tytuł: Integral of Continuous Functions of Two Variables Autorzy: Endou, Noboru; Shidama, Yasunari Abstrakt: We extend the formalization of the integral theory of onevariable functions for Riemann and Lebesgue integrals, showing that the Lebesgue integral of a continuous function of two variables coincides with the Riemann iterated integral of a projective function. 2023-01-01T00:00:00Z http://hdl.handle.net/11320/15863 Tytuł: Symmetrical Piecewise Linear Functions Composed by Absolute Value Function Autorzy: Mitsuishi, Takashi Abstrakt: We continue the formal development of the application of piecewise linear functions and centroids in the area of fuzzy set theory. The corresponding piecewise linear functions are symmetrical and composed by absolute function. In this paper we prove that the membership functions of isosceles triangle type and isosceles trapezoid type can be constructed by functions of this type. 2023-01-01T00:00:00Z