Journal & Issues

Volume 31 (2023): Issue 1 (September 2023)

Volume 30 (2022): Issue 4 (December 2022)

Volume 30 (2022): Issue 3 (October 2022)

Volume 30 (2022): Issue 2 (July 2022)

Volume 30 (2022): Issue 1 (April 2022)

Volume 29 (2021): Issue 4 (December 2021)

Volume 29 (2021): Issue 3 (September 2021)

Volume 29 (2021): Issue 2 (July 2021)

Volume 29 (2021): Issue 1 (April 2021)

Volume 28 (2020): Issue 4 (December 2020)

Volume 28 (2020): Issue 3 (October 2020)

Volume 28 (2020): Issue 2 (July 2020)

Volume 28 (2020): Issue 1 (April 2020)

Volume 27 (2019): Issue 4 (December 2019)

Volume 27 (2019): Issue 3 (October 2019)

Volume 27 (2019): Issue 2 (July 2019)

Volume 27 (2019): Issue 1 (April 2019)

Volume 26 (2018): Issue 4 (December 2018)

Volume 26 (2018): Issue 3 (October 2018)

Volume 26 (2018): Issue 2 (July 2018)

Volume 26 (2018): Issue 1 (April 2018)

Volume 25 (2017): Issue 4 (December 2017)

Volume 25 (2017): Issue 3 (October 2017)

Volume 25 (2017): Issue 2 (July 2017)

Volume 25 (2017): Issue 1 (March 2017)

Volume 24 (2016): Issue 4 (December 2016)

Volume 24 (2016): Issue 3 (September 2016)

Volume 24 (2016): Issue 2 (June 2016)

Volume 24 (2016): Issue 1 (March 2016)

Volume 23 (2015): Issue 4 (December 2015)

Volume 23 (2015): Issue 3 (September 2015)

Volume 23 (2015): Issue 2 (June 2015)

Volume 23 (2015): Issue 1 (March 2015)

Volume 22 (2014): Issue 4 (December 2014)

Volume 22 (2014): Issue 3 (September 2014)

Volume 22 (2014): Issue 2 (June 2014)
Special Issue: 25 years of the Mizar Mathematical Library

Volume 22 (2014): Issue 1 (March 2014)

Volume 21 (2013): Issue 4 (December 2013)

Volume 21 (2013): Issue 3 (October 2013)

Volume 21 (2013): Issue 2 (June 2013)

Volume 21 (2013): Issue 1 (January 2013)

Volume 20 (2012): Issue 4 (December 2012)

Volume 20 (2012): Issue 3 (December 2012)

Volume 20 (2012): Issue 2 (December 2012)

Volume 20 (2012): Issue 1 (January 2012)

Volume 19 (2011): Issue 4 (January 2011)

Volume 19 (2011): Issue 3 (January 2011)

Volume 19 (2011): Issue 2 (January 2011)

Volume 19 (2011): Issue 1 (January 2011)

Volume 18 (2010): Issue 4 (January 2010)

Volume 18 (2010): Issue 3 (January 2010)

Volume 18 (2010): Issue 2 (January 2010)

Volume 18 (2010): Issue 1 (January 2010)

Volume 17 (2009): Issue 4 (January 2009)

Volume 17 (2009): Issue 3 (January 2009)

Volume 17 (2009): Issue 2 (January 2009)

Volume 17 (2009): Issue 1 (January 2009)

Volume 16 (2008): Issue 4 (January 2008)

Volume 16 (2008): Issue 3 (January 2008)

Volume 16 (2008): Issue 2 (January 2008)

Volume 16 (2008): Issue 1 (January 2008)

Volume 15 (2007): Issue 4 (January 2007)

Volume 15 (2007): Issue 3 (January 2007)

Volume 15 (2007): Issue 2 (January 2007)

Volume 15 (2007): Issue 1 (January 2007)

Volume 14 (2006): Issue 4 (January 2006)

Volume 14 (2006): Issue 3 (January 2006)

Volume 14 (2006): Issue 2 (January 2006)

Volume 14 (2006): Issue 1 (January 2006)

Journal Details
Format
Journal
eISSN
1898-9934
ISSN
1426-2630
First Published
09 Jun 2008
Publication timeframe
4 times per year
Languages
English

Search

Volume 17 (2009): Issue 4 (January 2009)

Journal Details
Format
Journal
eISSN
1898-9934
ISSN
1426-2630
First Published
09 Jun 2008
Publication timeframe
4 times per year
Languages
English

Search

0 Articles
Open Access

Dilworth's Decomposition Theorem for Posets

Published Online: 08 Jul 2010
Page range: 223 - 232

Abstract

Dilworth's Decomposition Theorem for Posets

The following theorem is due to Dilworth [8]: Let P be a partially ordered set. If the maximal number of elements in an independent subset (anti-chain) of P is k, then P is the union of k chains (cliques).

In this article we formalize an elegant proof of the above theorem for finite posets by Perles [13]. The result is then used in proving the case of infinite posets following the original proof of Dilworth [8].

A dual of Dilworth's theorem also holds: a poset with maximum clique m is a union of m independent sets. The proof of this dual fact is considerably easier; we follow the proof by Mirsky [11]. Mirsky states also a corollary that a poset of r x s + 1 elements possesses a clique of size r + 1 or an independent set of size s + 1, or both. This corollary is then used to prove the result of Erdős and Szekeres [9].

Instead of using posets, we drop reflexivity and state the facts about anti-symmetric and transitive relations.

Open Access

Complex Integral

Published Online: 08 Jul 2010
Page range: 233 - 236

Abstract

Complex Integral

In this article, we defined complex curve and complex integral. Then we have proved the linearity for the complex integral. Furthermore, we have proved complex integral of complex curve's connection is the sum of each complex integral of individual complex curve.

Open Access

On the Lattice of Intervals and Rough Sets

Published Online: 08 Jul 2010
Page range: 237 - 244

Abstract

On the Lattice of Intervals and Rough Sets

Rough sets, developed by Pawlak [6], are an important tool to describe a situation of incomplete or partially unknown information. One of the algebraic models deals with the pair of the upper and the lower approximation. Although usually the tolerance or the equivalence relation is taken into account when considering a rough set, here we rather concentrate on the model with the pair of two definable sets, hence we are close to the notion of an interval set. In this article, the lattices of rough sets and intervals are formalized. This paper, being essentially the continuation of [3], is also a step towards the formalization of the algebraic theory of rough sets, as in [4] or [9].

Open Access

Basic Properties of Periodic Functions

Published Online: 08 Jul 2010
Page range: 245 - 248

Abstract

Basic Properties of Periodic Functions

In this article we present definitions, basic properties and some examples of periodic functions according to [5].

Open Access

Epsilon Numbers and Cantor Normal Form

Published Online: 08 Jul 2010
Page range: 249 - 256

Abstract

Epsilon Numbers and Cantor Normal Form

An epsilon number is a transfinite number which is a fixed point of an exponential map: ωϵ = ϵ. The formalization of the concept is done with use of the tetration of ordinals (Knuth's arrow notation, ↑). Namely, the ordinal indexing of epsilon numbers is defined as follows:

and for limit ordinal λ:

Tetration stabilizes at ω:

Every ordinal number α can be uniquely written as

where κ is a natural number, n1, n2, …, nk are positive integers, and β1 > β2 > … > βκ are ordinal numbers (βκ = 0). This decomposition of α is called the Cantor Normal Form of α.

0 Articles
Open Access

Dilworth's Decomposition Theorem for Posets

Published Online: 08 Jul 2010
Page range: 223 - 232

Abstract

Dilworth's Decomposition Theorem for Posets

The following theorem is due to Dilworth [8]: Let P be a partially ordered set. If the maximal number of elements in an independent subset (anti-chain) of P is k, then P is the union of k chains (cliques).

In this article we formalize an elegant proof of the above theorem for finite posets by Perles [13]. The result is then used in proving the case of infinite posets following the original proof of Dilworth [8].

A dual of Dilworth's theorem also holds: a poset with maximum clique m is a union of m independent sets. The proof of this dual fact is considerably easier; we follow the proof by Mirsky [11]. Mirsky states also a corollary that a poset of r x s + 1 elements possesses a clique of size r + 1 or an independent set of size s + 1, or both. This corollary is then used to prove the result of Erdős and Szekeres [9].

Instead of using posets, we drop reflexivity and state the facts about anti-symmetric and transitive relations.

Open Access

Complex Integral

Published Online: 08 Jul 2010
Page range: 233 - 236

Abstract

Complex Integral

In this article, we defined complex curve and complex integral. Then we have proved the linearity for the complex integral. Furthermore, we have proved complex integral of complex curve's connection is the sum of each complex integral of individual complex curve.

Open Access

On the Lattice of Intervals and Rough Sets

Published Online: 08 Jul 2010
Page range: 237 - 244

Abstract

On the Lattice of Intervals and Rough Sets

Rough sets, developed by Pawlak [6], are an important tool to describe a situation of incomplete or partially unknown information. One of the algebraic models deals with the pair of the upper and the lower approximation. Although usually the tolerance or the equivalence relation is taken into account when considering a rough set, here we rather concentrate on the model with the pair of two definable sets, hence we are close to the notion of an interval set. In this article, the lattices of rough sets and intervals are formalized. This paper, being essentially the continuation of [3], is also a step towards the formalization of the algebraic theory of rough sets, as in [4] or [9].

Open Access

Basic Properties of Periodic Functions

Published Online: 08 Jul 2010
Page range: 245 - 248

Abstract

Basic Properties of Periodic Functions

In this article we present definitions, basic properties and some examples of periodic functions according to [5].

Open Access

Epsilon Numbers and Cantor Normal Form

Published Online: 08 Jul 2010
Page range: 249 - 256

Abstract

Epsilon Numbers and Cantor Normal Form

An epsilon number is a transfinite number which is a fixed point of an exponential map: ωϵ = ϵ. The formalization of the concept is done with use of the tetration of ordinals (Knuth's arrow notation, ↑). Namely, the ordinal indexing of epsilon numbers is defined as follows:

and for limit ordinal λ:

Tetration stabilizes at ω:

Every ordinal number α can be uniquely written as

where κ is a natural number, n1, n2, …, nk are positive integers, and β1 > β2 > … > βκ are ordinal numbers (βκ = 0). This decomposition of α is called the Cantor Normal Form of α.