1. Home
  2. Formalized Mathematics
  3. Volume 19 (2011): Issue 1 (January 2011)

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 19 (2011): Issue 1 (January 2011)

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

Partial Differentiation of Vector-Valued Functions on n-Dimensional Real Normed Linear Spaces

Takao Inoué,
Takao Inoué,
Adam Naumowicz,
Adam Naumowicz,
Noboru Endou and
Noboru Endou and
Yasunari Shidama
Yasunari Shidama
Published Online: 18 Jul 2011
Page range: 1 - 9

Abstract

Partial Differentiation of Vector-Valued Functions on <italic>n</italic>-Dimensional Real Normed Linear Spaces

In this article, we define and develop partial differentiation of vector-valued functions on n-dimensional real normed linear spaces (refer to [19] and [20]).

Open Access

Some Properties of p-Groups and Commutative p-Groups

Xiquan Liang and
Xiquan Liang and
Dailu Li
Dailu Li
Published Online: 18 Jul 2011
Page range: 11 - 15

Abstract

Some Properties of <italic>p</italic>-Groups and Commutative <italic>p</italic>-Groups

This article describes some properties of p-groups and some properties of commutative p-groups.

Open Access

Riemann Integral of Functions from R into Real Normed Space

Keiichi Miyajima,
Keiichi Miyajima,
Takahiro Kato and
Takahiro Kato and
Yasunari Shidama
Yasunari Shidama
Published Online: 18 Jul 2011
Page range: 17 - 22

Abstract

Riemann Integral of Functions from R into Real Normed Space

In this article, we define the Riemann integral on functions from R into real normed space and prove the linearity of this operator. As a result, the Riemann integration can be applied to a wider range of functions. The proof method follows the [16].

Open Access

Normal Subgroup of Product of Groups

Hiroyuki Okazaki,
Hiroyuki Okazaki,
Kenichi Arai and
Kenichi Arai and
Yasunari Shidama
Yasunari Shidama
Published Online: 18 Jul 2011
Page range: 23 - 26

Abstract

Normal Subgroup of Product of Groups

In [6] it was formalized that the direct product of a family of groups gives a new group. In this article, we formalize that for all j ∈ I, the group G = Πi∈IGi has a normal subgroup isomorphic to Gj. Moreover, we show some relations between a family of groups and its direct product.

Open Access

The Mycielskian of a Graph

Piotr Rudnicki and
Piotr Rudnicki and
Lorna Stewart
Lorna Stewart
Published Online: 18 Jul 2011
Page range: 27 - 34

Abstract

The Mycielskian of a Graph

Let ω(G) and χ(G) be the clique number and the chromatic number of a graph G. Mycielski [11] presented a construction that for any n creates a graph Mn which is triangle-free (ω(G) = 2) with χ(G) > n. The starting point is the complete graph of two vertices (K2). M(n+1) is obtained from Mn through the operation μ(G) called the Mycielskian of a graph G.

We first define the operation μ(G) and then show that ω(μ(G)) = ω(G) and χ(μ(G)) = χ(G) + 1. This is done for arbitrary graph G, see also [10]. Then we define the sequence of graphs Mn each of exponential size in n and give their clique and chromatic numbers.

Open Access

Difference and Difference Quotient. Part IV

Xiquan Liang,
Xiquan Liang,
Ling Tang and
Ling Tang and
Xichun Jiang
Xichun Jiang
Published Online: 18 Jul 2011
Page range: 35 - 39

Abstract

Difference and Difference Quotient. Part IV

In this article, we give some important theorems of forward difference, backward difference, central difference and difference quotient and forward difference, backward difference, central difference and difference quotient formulas of some special functions.

Open Access

The Definition of Topological Manifolds

Marco Riccardi
Marco Riccardi
Published Online: 18 Jul 2011
Page range: 41 - 44

Abstract

The Definition of Topological Manifolds

This article introduces the definition of n-locally Euclidean topological spaces and topological manifolds [13].

Open Access

More on Continuous Functions on Normed Linear Spaces

Hiroyuki Okazaki,
Hiroyuki Okazaki,
Noboru Endou and
Noboru Endou and
Yasunari Shidama
Yasunari Shidama
Published Online: 18 Jul 2011
Page range: 45 - 49

Abstract

More on Continuous Functions on Normed Linear Spaces

In this article we formalize the definition and some facts about continuous functions from R into normed linear spaces [14].

Open Access

Cartesian Products of Family of Real Linear Spaces

Hiroyuki Okazaki,
Hiroyuki Okazaki,
Noboru Endou and
Noboru Endou and
Yasunari Shidama
Yasunari Shidama
Published Online: 18 Jul 2011
Page range: 51 - 59

Abstract

Cartesian Products of Family of Real Linear Spaces

In this article we introduced the isomorphism mapping between cartesian products of family of linear spaces [4]. Those products had been formalized by two different ways, i.e., the way using the functor [:X, Y:] and ones using the functor "product". By the same way, the isomorphism mapping was defined between Cartesian products of family of linear normed spaces also.

Open Access

Formalization of Integral Linear Space

Yuichi Futa,
Yuichi Futa,
Hiroyuki Okazaki and
Hiroyuki Okazaki and
Yasunari Shidama
Yasunari Shidama
Published Online: 18 Jul 2011
Page range: 61 - 64

Abstract

Formalization of Integral Linear Space

In this article, we formalize integral linear spaces, that is a linear space with integer coefficients. Integral linear spaces are necessary for lattice problems, LLL (Lenstra-Lenstra-Lovász) base reduction algorithm that outputs short lattice base and cryptographic systems with lattice [8].

0 Articles
Open Access

Partial Differentiation of Vector-Valued Functions on n-Dimensional Real Normed Linear Spaces

Takao Inoué,
Takao Inoué,
Adam Naumowicz,
Adam Naumowicz,
Noboru Endou and
Noboru Endou and
Yasunari Shidama
Yasunari Shidama
Published Online: 18 Jul 2011
Page range: 1 - 9

Abstract

Partial Differentiation of Vector-Valued Functions on <italic>n</italic>-Dimensional Real Normed Linear Spaces

In this article, we define and develop partial differentiation of vector-valued functions on n-dimensional real normed linear spaces (refer to [19] and [20]).

Open Access

Some Properties of p-Groups and Commutative p-Groups

Xiquan Liang and
Xiquan Liang and
Dailu Li
Dailu Li
Published Online: 18 Jul 2011
Page range: 11 - 15

Abstract

Some Properties of <italic>p</italic>-Groups and Commutative <italic>p</italic>-Groups

This article describes some properties of p-groups and some properties of commutative p-groups.

Open Access

Riemann Integral of Functions from R into Real Normed Space

Keiichi Miyajima,
Keiichi Miyajima,
Takahiro Kato and
Takahiro Kato and
Yasunari Shidama
Yasunari Shidama
Published Online: 18 Jul 2011
Page range: 17 - 22

Abstract

Riemann Integral of Functions from R into Real Normed Space

In this article, we define the Riemann integral on functions from R into real normed space and prove the linearity of this operator. As a result, the Riemann integration can be applied to a wider range of functions. The proof method follows the [16].

Open Access

Normal Subgroup of Product of Groups

Hiroyuki Okazaki,
Hiroyuki Okazaki,
Kenichi Arai and
Kenichi Arai and
Yasunari Shidama
Yasunari Shidama
Published Online: 18 Jul 2011
Page range: 23 - 26

Abstract

Normal Subgroup of Product of Groups

In [6] it was formalized that the direct product of a family of groups gives a new group. In this article, we formalize that for all j ∈ I, the group G = Πi∈IGi has a normal subgroup isomorphic to Gj. Moreover, we show some relations between a family of groups and its direct product.

Open Access

The Mycielskian of a Graph

Piotr Rudnicki and
Piotr Rudnicki and
Lorna Stewart
Lorna Stewart
Published Online: 18 Jul 2011
Page range: 27 - 34

Abstract

The Mycielskian of a Graph

Let ω(G) and χ(G) be the clique number and the chromatic number of a graph G. Mycielski [11] presented a construction that for any n creates a graph Mn which is triangle-free (ω(G) = 2) with χ(G) > n. The starting point is the complete graph of two vertices (K2). M(n+1) is obtained from Mn through the operation μ(G) called the Mycielskian of a graph G.

We first define the operation μ(G) and then show that ω(μ(G)) = ω(G) and χ(μ(G)) = χ(G) + 1. This is done for arbitrary graph G, see also [10]. Then we define the sequence of graphs Mn each of exponential size in n and give their clique and chromatic numbers.

Open Access

Difference and Difference Quotient. Part IV

Xiquan Liang,
Xiquan Liang,
Ling Tang and
Ling Tang and
Xichun Jiang
Xichun Jiang
Published Online: 18 Jul 2011
Page range: 35 - 39

Abstract

Difference and Difference Quotient. Part IV

In this article, we give some important theorems of forward difference, backward difference, central difference and difference quotient and forward difference, backward difference, central difference and difference quotient formulas of some special functions.

Open Access

The Definition of Topological Manifolds

Marco Riccardi
Marco Riccardi
Published Online: 18 Jul 2011
Page range: 41 - 44

Abstract

The Definition of Topological Manifolds

This article introduces the definition of n-locally Euclidean topological spaces and topological manifolds [13].

Open Access

More on Continuous Functions on Normed Linear Spaces

Hiroyuki Okazaki,
Hiroyuki Okazaki,
Noboru Endou and
Noboru Endou and
Yasunari Shidama
Yasunari Shidama
Published Online: 18 Jul 2011
Page range: 45 - 49

Abstract

More on Continuous Functions on Normed Linear Spaces

In this article we formalize the definition and some facts about continuous functions from R into normed linear spaces [14].

Open Access

Cartesian Products of Family of Real Linear Spaces

Hiroyuki Okazaki,
Hiroyuki Okazaki,
Noboru Endou and
Noboru Endou and
Yasunari Shidama
Yasunari Shidama
Published Online: 18 Jul 2011
Page range: 51 - 59

Abstract

Cartesian Products of Family of Real Linear Spaces

In this article we introduced the isomorphism mapping between cartesian products of family of linear spaces [4]. Those products had been formalized by two different ways, i.e., the way using the functor [:X, Y:] and ones using the functor "product". By the same way, the isomorphism mapping was defined between Cartesian products of family of linear normed spaces also.

Open Access

Formalization of Integral Linear Space

Yuichi Futa,
Yuichi Futa,
Hiroyuki Okazaki and
Hiroyuki Okazaki and
Yasunari Shidama
Yasunari Shidama
Published Online: 18 Jul 2011
Page range: 61 - 64

Abstract

Formalization of Integral Linear Space

In this article, we formalize integral linear spaces, that is a linear space with integer coefficients. Integral linear spaces are necessary for lattice problems, LLL (Lenstra-Lenstra-Lovász) base reduction algorithm that outputs short lattice base and cryptographic systems with lattice [8].