Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 32

Liczba wyników na stronie
first rewind previous Strona / 2 next fast forward last

Wyniki wyszukiwania

help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 2 next fast forward last
1
Content available remote

The Correspondence Betweenn-dimensional Euclidean Space and the Product ofnReal Lines

100%
Korniłowicz A.
Formalized Mathematics
|
2010
|
tom 18
|
nr 1
81-85
EN
In the article we prove that a family of open n-hypercubes is a basis of n-dimensional Euclidean space. The equality of the space and the product of n real lines has been proven.
2
Content available remote

Cayley's Theorem

100%
Korniłowicz A.
Formalized Mathematics
|
2011
|
tom 19
|
nr 4
223-225
EN
The article formalizes the Cayley's theorem saying that every group G is isomorphic to a subgroup of the symmetric group on G.
3
Content available remote

Arithmetic Operations on Functions from Sets into Functional Sets

100%
Korniłowicz A.
Formalized Mathematics
|
2009
|
tom 17
|
nr 1
43-60
EN
In this paper we introduce sets containing number-valued functions. Different arithmetic operations on maps between any set and such functional sets are later defined.MML identifier: VALUED 2, version: 7.11.01 4.117.1046
4
Content available remote

Differentiability of Polynomials over Reals

100%
Korniłowicz A.
Formalized Mathematics
|
2017
|
tom 25
|
nr 1
31-37
EN
In this article, we formalize in the Mizar system [3] the notion of the derivative of polynomials over the field of real numbers [4]. To define it, we use the derivative of functions between reals and reals [9].
5
Content available remote

On the Continuity of Some Functions

100%
Korniłowicz A.
Formalized Mathematics
|
2010
|
tom 18
|
nr 3
175-183
EN
We prove that basic arithmetic operations preserve continuity of functions.
6
Content available remote

Mazur-Ulam Theorem

100%
Korniłowicz A.
Formalized Mathematics
|
2011
|
tom 19
|
nr 3
127-130
EN
The Mazur-Ulam theorem [15] has been formulated as two registrations: cluster bijective isometric -> midpoints-preserving Function of E, F; and cluster isometric midpoints-preserving -> Affine Function of E, F; A proof given by Jussi Väisälä [23] has been formalized.
7
Content available remote

Miscellaneous Facts about Open Functions and Continuous Functions

100%
Korniłowicz A.
Formalized Mathematics
|
2010
|
tom 18
|
nr 3
171-174
EN
In this article we give definitions of open functions and continuous functions formulated in terms of "balls" of given topological spaces.
8
Content available remote

Collective Operations on Number-Membered Sets

100%
Korniłowicz A.
Formalized Mathematics
|
2009
|
tom 17
|
nr 2
99-115
EN
The article starts with definitions of sets of opposite and inverse numbers of a given number membered set. Next, collective addition, subtraction, multiplication and division of two sets are defined. Complex numbers cases and extended real numbers ones are introduced separately and unified for reals. Shortcuts for singletons cases are also defined.
9
Content available remote

Commutativeness of Fundamental Groups of Topological Groups

100%
Korniłowicz A.
Formalized Mathematics
|
2013
|
tom 21
|
nr 2
127-131
EN
In this article we prove that fundamental groups based at the unit point of topological groups are commutative [11].
10
Content available remote

Products in Categories without Uniqueness of cod and dom

100%
Korniłowicz A.
Formalized Mathematics
|
2012
|
tom 20
|
nr 4
303-307
EN
The paper introduces Cartesian products in categories without uniqueness of cod and dom. It is proven that set-theoretical product is the product in the category Ens [7].
11
Content available remote

Cayley-Dickson Construction

100%
Korniłowicz A.
Formalized Mathematics
|
2012
|
tom 20
|
nr 4
281-290
EN
Cayley-Dickson construction produces a sequence of normed algebras over real numbers. Its consequent applications result in complex numbers, quaternions, octonions, etc. In this paper we formalize the construction and prove its basic properties.
12
Content available remote

Basic Operations on Preordered Coherent Spaces

64%
Grue K., Korniłowicz A.
Formalized Mathematics
|
2007
|
tom 15
|
nr 4
213-230
EN
This Mizar paper presents the definition of a "Preordered Coherent Space" (PCS). Furthermore, the paper defines a number of operations on PCS's and states and proves a number of elementary lemmas about these operations. PCS's have many useful properties which could qualify them for mathematical study in their own right. PCS's were invented, however, to construct Scott domains, to solve domain equations, and to construct models of various versions of lambda calculus.For more on PCS's, see [11]. The present Mizar paper defines the operations on PCS's used in Chapter 8 of [3].
13
Content available remote

Introduction to Liouville Numbers

64%
Grabowski A., Korniłowicz A.
Formalized Mathematics
|
2017
|
tom 25
|
nr 1
39-48
EN
The article defines Liouville numbers, originally introduced by Joseph Liouville in 1844 [17] as an example of an object which can be approximated “quite closely” by a sequence of rational numbers. A real number x is a Liouville number iff for every positive integer n, there exist integers p and q such that q > 1 and [...] It is easy to show that all Liouville numbers are irrational. Liouville constant, which is also defined formally, is the first transcendental (not algebraic) number. It is defined in Section 6 quite generally as the sum [...] for a finite sequence {ak}k∈ℕ and b ∈ ℕ. Based on this definition, we also introduced the so-called Liouville number as [...] substituting in the definition of L(ak, b) the constant sequence of 1’s and b = 10. Another important examples of transcendental numbers are e and π [7], [13], [6]. At the end, we show that the construction of an arbitrary Lioville constant satisfies the properties of a Liouville number [12], [1]. We show additionally, that the set of all Liouville numbers is infinite, opening the next item from Abad and Abad’s list of “Top 100 Theorems”. We show also some preliminary constructions linking real sequences and finite sequences, where summing formulas are involved. In the Mizar [14] proof, we follow closely https://en.wikipedia.org/wiki/Liouville_number. The aim is to show that all Liouville numbers are transcendental.
14
Content available remote

Basel Problem – Preliminaries

64%
Korniłowicz A., Pąk K.
Formalized Mathematics
|
2017
|
tom 25
|
nr 2
141-147
EN
In the article we formalize in the Mizar system [4] preliminary facts needed to prove the Basel problem [7, 1]. Facts that are independent from the notion of structure are included here.
15
Content available remote

Basel Problem

64%
Pąk K., Korniłowicz A.
Formalized Mathematics
|
2017
|
tom 25
|
nr 2
149-155
EN
A rigorous elementary proof of the Basel problem [6, 1] ∑n=1∞1n2=π26 $$\sum\nolimits_{n = 1}^\infty {{1 \over {n^2 }} = {{\pi ^2 } \over 6}} $$ is formalized in the Mizar system [3]. This theorem is item #14 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.
16
Content available remote

Vieta’s Formula about the Sum of Roots of Polynomials

64%
Korniłowicz A., Pąk K.
Formalized Mathematics
|
2017
|
tom 25
|
nr 2
87-92
EN
In the article we formalized in the Mizar system [2] the Vieta formula about the sum of roots of a polynomial anxn + an−1xn−1 + ··· + a1x + a0 defined over an algebraically closed field. The formula says that [...] x1+x2+⋯+xn−1+xn=−an−1an $x_1 + x_2 + \cdots + x_{n - 1} + x_n = - {{a_{n - 1} } \over {a_n }}$ , where x1, x2,…, xn are (not necessarily distinct) roots of the polynomial [12]. In the article the sum is denoted by SumRoots.
17
Content available remote

Pseudo-Canonical Formulae are Classical

64%
Caminati M. B., Korniłowicz A.
Formalized Mathematics
|
2014
|
tom 22
|
nr 2
99-103
EN
An original result about Hilbert Positive Propositional Calculus introduced in [11] is proven. That is, it is shown that the pseudo-canonical formulae of that calculus (and hence also the canonical ones, see [17]) are a subset of the classical tautologies.
18
Content available remote

The Borsuk-Ulam Theorem

64%
Korniłowicz A., Riccardi M.
Formalized Mathematics
|
2012
|
tom 20
|
nr 2
105-112
EN
The Borsuk-Ulam theorem about antipodals is proven, [18, pp. 32-33].
19
Content available remote

Niven’s Theorem

64%
Korniłowicz A., Naumowicz A.
Formalized Mathematics
|
2016
|
tom 24
|
nr 4
301-308
EN
This article formalizes the proof of Niven’s theorem [12] which states that if x/π and sin(x) are both rational, then the sine takes values 0, ±1/2, and ±1. The main part of the formalization follows the informal proof presented at Pr∞fWiki (https://proofwiki.org/wiki/Niven’s_Theorem#Source_of_Name). For this proof, we have also formalized the rational and integral root theorems setting constraints on solutions of polynomial equations with integer coefficients [8, 9].
20
Content available remote

Fundamental Group of n-sphere for n ≥ 2

64%
Riccardi M., Korniłowicz A.
Formalized Mathematics
|
2012
|
tom 20
|
nr 2
97-104
EN
Triviality of fundamental groups of spheres of dimension greater than 1 is proven, [17]
first rewind previous Strona / 2 next fast forward last
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ć.