DSpace Kolekcja:http://hdl.handle.net/11320/153992026-06-01T15:18:35Z2026-06-01T15:18:35ZExtensions of OrderingsSchwarzweller, Christophhttp://hdl.handle.net/11320/158672024-01-26T11:54:49Z2023-01-01T00:00:00ZTytuł: 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:00ZTarski Geometry Axioms. Part V – Half-planes and PlanesCoghetto, RolandGrabowski, Adamhttp://hdl.handle.net/11320/158662024-01-26T11:28:51Z2023-01-01T00:00:00ZTytuł: 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:00ZIntegral of Continuous Functions of Two VariablesEndou, NoboruShidama, Yasunarihttp://hdl.handle.net/11320/158642024-01-26T10:44:45Z2023-01-01T00:00:00ZTytuł: 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:00ZSymmetrical Piecewise Linear Functions Composed by Absolute Value FunctionMitsuishi, Takashihttp://hdl.handle.net/11320/158632024-01-26T10:19:07Z2023-01-01T00:00:00ZTytuł: 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