DSpace Zespół:
http://hdl.handle.net/11320/3332
Sun, 04 Aug 2024 04:39:23 GMT2024-08-04T04:39:23ZExtensions of Orderings
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.Sun, 01 Jan 2023 00:00:00 GMThttp://hdl.handle.net/11320/158672023-01-01T00:00:00ZTarski Geometry Axioms. Part V – Half-planes and Planes
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.Sun, 01 Jan 2023 00:00:00 GMThttp://hdl.handle.net/11320/158662023-01-01T00:00:00ZIntegral of Continuous Functions of Two Variables
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.Sun, 01 Jan 2023 00:00:00 GMThttp://hdl.handle.net/11320/158642023-01-01T00:00:00ZSymmetrical Piecewise Linear Functions Composed by Absolute Value Function
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.Sun, 01 Jan 2023 00:00:00 GMThttp://hdl.handle.net/11320/158632023-01-01T00:00:00Z