MML Query (home page)

Mizar project at Bialystok Technical University
page generated with MMLQT (MML Query Transformation) tool
Mizar home, download
files: abstr, articles,
bin, doc, emacs gabs, fmbibs, gabs (more) semantic MML
Megrez
MML Query (beta)

Template maker
Mizar TWiki
MML Query server
Megrez services
Journals:
   FM: MetaPRESS, server, proof-read
   MM&A (preparation)
Syntax: xml, html
Downloads
Mizar syntax, xml, txt
MML 4.145.1096
- most important facts MML links Monographs
Conference MKM2004
Workshop 30 years of Mizar
dydaktyka (e-learning)
Mizar Mathematical Library (version 4.145.1096) includes 1093 articles written by 229 authors and 50173 theorems, 9589 definitions, 772 schemes, 9565 registrations, 6945 symbols. (more statistics, other versions)
New:      monograph: TG Set Theory      authors by # of important facts
MML links:

Latest 30 articles (the query: list of article ordered by historical order reversed select 0-29)
  1. integr18: Riemann Integral of Functions from $\mathbbbR$ into Real Normed Space by Keiichi Miyajima, Takahiro Kato, Yasunari Shidama (submitted May 20, 2010)
    18 theorems, 9 definitions, no schemes, no registrations, abstract, semantically linked , full article, gab.

  2. groupp_1: Some Properties of $p$-Groups and Commutative $p$-Groups by Xiquan Liang, Dailu Li (submitted April 29, 2010)
    36 theorems, 4 definitions, no schemes, 21 registrations, abstract, semantically linked , full article, gab.

  3. pdiff_7: Partial Differentiation of Vector-Valued Functions on $n$-Dimensional Real Normed Linear Spaces by Takao Inoue, Adam Naumowicz, Noboru Endou, Yasunari Shidama (submitted April 22, 2010)
    49 theorems, 7 definitions, no schemes, no registrations, abstract, semantically linked , full article, gab.

  4. ami_wstd: Weakly Standard Ordering of Instruction Locations by Andrzej Trybulec, Piotr Rudnicki, Artur Kornilowicz (submitted April 22, 2010)
    36 theorems, 14 definitions, no schemes, 12 registrations, abstract, semantically linked , full article, gab.

  5. normsp_0: Preliminaries to Normed Spaces by Andrzej Trybulec (submitted March 23, 2010)
    no theorems, 6 definitions, no schemes, 7 registrations, abstract, semantically linked , full article, gab.

  6. random_2: Probability Measure on Discrete Spaces and Algebra of Real Valued Random Variables by Hiroyuki, Okazaki, Yasunari Shidama (submitted March 16, 2010)
    17 theorems, 4 definitions, no schemes, 4 registrations, abstract, semantically linked , full article, gab.

  7. pdiff_6: Differentiation of Vector-Valued Functions on $n$-Dimensional Real Normed Linear Spaces by Takao Inoue, Noboru Endou, Yasunari Shidama (submitted February 23, 2010)
    33 theorems, 4 definitions, no schemes, 4 registrations, abstract, semantically linked , full article, gab.

  8. integr16: Riemann Integral of Functions $\mathbbbR$ into $\mathbbbC$ by Keiichi Miyajima, Takahiro Kato, Yasunari Shidama (submitted February 23, 2010)
    23 theorems, 9 definitions, no schemes, 4 registrations, abstract, semantically linked , full article, gab.

  9. cardfin2: Counting Derangements, Counting Non Bijective Functions and the Birthday Problem by Cezary Kaliszyk (submitted February 23, 2010)
    18 theorems, 4 definitions, 1 scheme, 8 registrations, abstract, semantically linked , full article, gab.

  10. simplex1: Sperner's Lemma by Karol Pak (submitted February 9, 2010)
    47 theorems, 8 definitions, no schemes, 19 registrations, abstract, semantically linked , full article, gab.

  11. rlaffin2: The Geometric Interior in Real Linear Spaces by Karol Pak (submitted February 9, 2010)
    30 theorems, 2 definitions, no schemes, 1 registration, abstract, semantically linked , full article, gab.

  12. toprealc: On the Continuity of Some Functions by Artur Kornilowicz (submitted February 9, 2010)
    62 theorems, 6 definitions, no schemes, 54 registrations, abstract, semantically linked , full article, gab.

  13. tops_4: Miscellaneous Facts about Open Functions and Continuous Functions by Artur Kornilowicz (submitted February 9, 2010)
    25 theorems, no definitions, no schemes, no registrations, abstract, semantically linked , full article, gab.

  14. lpspace2: On $L^p$ Space Formed by Real-valued Partial Functions by Yasushige Watase, Noboru Endou, Yasunari Shidama (submitted February 4, 2010)
    78 theorems, 13 definitions, no schemes, 11 registrations, abstract, semantically linked , full article, gab.

  15. integr14: Integrability Formulas -- Part III by Bo Li, Na Ma (submitted February 4, 2010)
    59 theorems, no definitions, no schemes, no registrations, abstract, semantically linked , full article, gab.

  16. integr13: Integrability Formulas -- Part II by Bo Li, Na Ma, Xiquan Liang (submitted February 4, 2010)
    57 theorems, no definitions, no schemes, no registrations, abstract, semantically linked , full article, gab.

  17. pdiff_5: Second-order Partial Differentiation of Real Ternary Functions by Takao Inoue (submitted January 26, 2010)
    84 theorems, 36 definitions, no schemes, no registrations, abstract, semantically linked , full article, gab.

  18. rvsum_2: The Sum and Product of Finite Sequences of Complex Numbers by Keiichi Miyajima, Takahiro Kato (submitted January 12, 2010)
    54 theorems, 6 definitions, no schemes, 1 registration, abstract, semantically linked , full article, gab.

  19. simplex0: Abstract Simplicial Complexes by Karol Pak (submitted December 18, 2009)
    65 theorems, 21 definitions, no schemes, 63 registrations, abstract, semantically linked , full article, gab.

  20. rlaffin1: Affine Indepedence in Vector Spaces by Karol Pak (submitted December 18, 2009)
    84 theorems, 7 definitions, no schemes, 16 registrations, abstract, semantically linked , full article, gab.

  21. euclid_9: The Correspondence Between $n$-dimensional Euclidean Space and the Product of $n$ Real Lines by Artur Kornilowicz (submitted November 30, 2009)
    28 theorems, 5 definitions, no schemes, 37 registrations, abstract, semantically linked , full article, gab.

  22. fib_num4: Representation of the Fibonacci and Lucas Numbers in Terms of the Floor and Ceiling Functor by Magdalena Jastrzebska (submitted November 30, 2009)
    39 theorems, no definitions, no schemes, no registrations, abstract, semantically linked , full article, gab.

  23. abcmiz_a: A Model of Mizar Concepts -- Unification by Grzegorz Bancerek (submitted November 20, 2009)
    60 theorems, 30 definitions, 3 schemes, 32 registrations, abstract, semantically linked , full article, gab.

  24. diff_3: Difference and Difference Quotient -- Part III by Xiquan Liang, Ling Tang (submitted November 17, 2009)
    96 theorems, no definitions, no schemes, no registrations, abstract, semantically linked , full article, gab.

  25. grnilp_1: Nilpotent Groups by Dailu Li, Xiquan Liang, Yanhong Men (submitted November 10, 2009)
    29 theorems, 2 definitions, no schemes, 8 registrations, abstract, semantically linked , full article, gab.

  26. poset_1: Fix-point Theorem for Continuous Functions on Chain-complete Posets by Kazuhisa Ishida, Yasunari Shidama (submitted November 10, 2009)
    12 theorems, 12 definitions, no schemes, 12 registrations, abstract, semantically linked , full article, gab.

  27. pdiff_4: Partial Differentiation of Real Ternary Functions by Takao Inoue, Bing Xie, Xiquan Liang (submitted November 7, 2009)
    43 theorems, 10 definitions, no schemes, no registrations, abstract, semantically linked , full article, gab.

  28. integr12: Integrability Formulas -- Part I by Bo Li, Na Ma (submitted November 7, 2009)
    45 theorems, no definitions, no schemes, no registrations, abstract, semantically linked , full article, gab.

  29. algstr_4: Free Magmas by Marco Riccardi (submitted October 20, 2009)
    48 theorems, 21 definitions, 4 schemes, 26 registrations, abstract, semantically linked , full article, gab.

  30. c0sp2: Banach Algebra of Continuous Functionals by Kanazashi Katuhiko, Noboru Endou, Yasunari Shidama (submitted October 20, 2009)
    22 theorems, 5 definitions, no schemes, 12 registrations, abstract, semantically linked , full article, gab.


Full list in reversed historical order (start querying) and lexical order of MML Id, titles, authors.
  1. version 4.145.1096
  2. version 4.137.1092 [differences]
  3. version 4.133.1080 [differences]
  4. version 4.130.1076 [differences]
  5. version 4.117.1046 [differences]
[Compare two versions]
Grzegorz Bancerek: bancerek (at) mizar.org