1. Home
  2. Formalized Mathematics
  3. Volume 15 (2007): Issue 2 (January 2007)

Issues

Journal & Issues

Formalized Mathematics's Cover Image
Formalized Mathematics

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 15 (2007): Issue 2 (January 2007)

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

Combinatorial Grassmannians

Andrzej Owsiejczuk
Andrzej Owsiejczuk
Published Online: 09 Jun 2008
Page range: 27 - 33

Abstract

Combinatorial Grassmannians

In the paper I construct the configuration G which is a partial linear space. It consists of k-element subsets of some base set as points and (k + 1)-element subsets as lines. The incidence is given by inclusion. I also introduce automorphisms of partial linear spaces and show that automorphisms of G are generated by permutations of the base set.

Open Access

The Jordan-Hölder Theorem

Marco Riccardi
Marco Riccardi
Published Online: 09 Jun 2008
Page range: 35 - 51

Abstract

The Jordan-Hölder Theorem

The goal of this article is to formalize the Jordan-Hölder theorem in the context of group with operators as in the book [5]. Accordingly, the article introduces the structure of group with operators and reformulates some theorems on a group already present in the Mizar Mathematical Library. Next, the article formalizes the Zassenhaus butterfly lemma and the Schreier refinement theorem, and defines the composition series.

Open Access

Regular Expression Quantifiers — m to n Occurrences

Michał Trybulec
Michał Trybulec
Published Online: 09 Jun 2008
Page range: 53 - 58

Abstract

Regular Expression Quantifiers — <italic>m</italic> to <italic>n</italic> Occurrences

This article includes proofs of several facts that are supplemental to the theorems proved in [10]. Next, it builds upon that theory to extend the framework for proving facts about formal languages in general and regular expression operators in particular. In this article, two quantifiers are defined and their properties are shown: m to n occurrences (or the union of a range of powers) and optional occurrence. Although optional occurrence is a special case of the previous operator (0 to 1 occurrences), it is often defined in regex applications as a separate operator - hence its explicit definition and properties in the article. Notation and terminology were taken from [13].

Open Access

Riemann Indefinite Integral of Functions of Real Variable

Yasunari Shidama,
Yasunari Shidama,
Noboru Endou and
Noboru Endou and
Katsumi Wasaki
Katsumi Wasaki
Published Online: 09 Jun 2008
Page range: 59 - 63

Abstract

Riemann Indefinite Integral of Functions of Real Variable

In this article we define the Riemann indefinite integral of functions of real variable and prove the linearity of that [1]. And we give some examples of the indefinite integral of some elementary functions. Furthermore, also the theorem about integral operation and uniform convergent sequence of functions is proved.

Open Access

Partial Differentiation on Normed Linear Spaces Rn

Noboru Endou,
Noboru Endou,
Yasunari Shidama and
Yasunari Shidama and
Keiichi Miyajima
Keiichi Miyajima
Published Online: 09 Jun 2008
Page range: 65 - 72

Abstract

Partial Differentiation on Normed Linear Spaces <italic>R<sup>n</sup></italic>

Summary. In this article, we define the partial differentiation of functions of real variable and prove the linearity of this operator [18].

0 Articles
Open Access

Combinatorial Grassmannians

Andrzej Owsiejczuk
Andrzej Owsiejczuk
Published Online: 09 Jun 2008
Page range: 27 - 33

Abstract

Combinatorial Grassmannians

In the paper I construct the configuration G which is a partial linear space. It consists of k-element subsets of some base set as points and (k + 1)-element subsets as lines. The incidence is given by inclusion. I also introduce automorphisms of partial linear spaces and show that automorphisms of G are generated by permutations of the base set.

Open Access

The Jordan-Hölder Theorem

Marco Riccardi
Marco Riccardi
Published Online: 09 Jun 2008
Page range: 35 - 51

Abstract

The Jordan-Hölder Theorem

The goal of this article is to formalize the Jordan-Hölder theorem in the context of group with operators as in the book [5]. Accordingly, the article introduces the structure of group with operators and reformulates some theorems on a group already present in the Mizar Mathematical Library. Next, the article formalizes the Zassenhaus butterfly lemma and the Schreier refinement theorem, and defines the composition series.

Open Access

Regular Expression Quantifiers — m to n Occurrences

Michał Trybulec
Michał Trybulec
Published Online: 09 Jun 2008
Page range: 53 - 58

Abstract

Regular Expression Quantifiers — <italic>m</italic> to <italic>n</italic> Occurrences

This article includes proofs of several facts that are supplemental to the theorems proved in [10]. Next, it builds upon that theory to extend the framework for proving facts about formal languages in general and regular expression operators in particular. In this article, two quantifiers are defined and their properties are shown: m to n occurrences (or the union of a range of powers) and optional occurrence. Although optional occurrence is a special case of the previous operator (0 to 1 occurrences), it is often defined in regex applications as a separate operator - hence its explicit definition and properties in the article. Notation and terminology were taken from [13].

Open Access

Riemann Indefinite Integral of Functions of Real Variable

Yasunari Shidama,
Yasunari Shidama,
Noboru Endou and
Noboru Endou and
Katsumi Wasaki
Katsumi Wasaki
Published Online: 09 Jun 2008
Page range: 59 - 63

Abstract

Riemann Indefinite Integral of Functions of Real Variable

In this article we define the Riemann indefinite integral of functions of real variable and prove the linearity of that [1]. And we give some examples of the indefinite integral of some elementary functions. Furthermore, also the theorem about integral operation and uniform convergent sequence of functions is proved.

Open Access

Partial Differentiation on Normed Linear Spaces Rn

Noboru Endou,
Noboru Endou,
Yasunari Shidama and
Yasunari Shidama and
Keiichi Miyajima
Keiichi Miyajima
Published Online: 09 Jun 2008
Page range: 65 - 72

Abstract

Partial Differentiation on Normed Linear Spaces <italic>R<sup>n</sup></italic>

Summary. In this article, we define the partial differentiation of functions of real variable and prove the linearity of this operator [18].