Formalized Mathematics
Table of Contents
Volume 1(1), 1990
Tarski Grothendieck Set Theory
Built-in Concepts
Boolean Properties of Sets
Enumerated Sets
Basic Properties of Real Numbers
The Fundamental Properties of Natural Numbers
Some Basic Properties of Sets
Functions and Their Basic Properties
Properties of Subsets
Relations and Their Basic Properties
Properties of Binary Relations
The Ordinal Numbers
Tuples, Projections and Cartesian Products
Segments of Natural Numbers and Finite Sequences
Domains and Their Cartesian Products
The Well Ordering Relations
A Model of ZF Set Theory Language
Families of Sets
Functions from a Set to a Set
Finite Sets
Graphs of Functions
Binary Operations
Relations Defined on Sets
Boolean Domains
Models and Satisfiability
The Contraction Lemma
Axioms of Incidency
Introduction to Lattice Theory
Topological Spaces and Continuous Functions
Subsets of Topological Spaces
Connected Spaces
Basic Functions and Operations on Functions
Volume 1(2)
Families of Subsets, Subspaces and Mappings in Topological Spaces
Some Properties of Functions Modul and Signum
Zermelo Theorem and Axiom of Choice
Real Sequences and Basic Operations on Them
Convergent Sequences and the Limit of Sequences
Properties of ZF Models
Sequences of Ordinal Numbers
Vectors in Real Linear Space
Subspaces and Cosets of Subspaces in Real Linear Arithmetic
A First Order Language
Partially Ordered Sets
Recursive Definitions
Binary Operations Applied to Functions
Abelian Groups, Fields, and Vector Spaces
Parallelity Spaces
Construction of a bilinear antisymmetric form in symplectic vector space
Construction of a bilinear symmetric form in orthogonal vector space
Partial Functions
Semilattice Operations on Finite Subsets
Cardinal Numbers
Compact Spaces
Kuratowski-Zorn Lemma
Operations on Subspaces in Real Linear Space
Sigma-Fields and Probability
Introduction to Categories and Functors
Introduction to Trees
Volume 1(3)
Zermelo's Theorem
Group and Field Definitions
Equivalence Relations and Classes of Abstraction
Some Properties of Real Numbers
Connectives and Subformulae of the First Order Language
Variables in Formulae of the First Order Language
Monotone Real Sequences. Subsequences
Convergent Real Sequences. Upper and Lower Bound of Sets of Real Numbers
Midpoint algebras
The Fundamental Logic Structure in Quantum Mechanics
Function Domains and Fraenkel Operator
Integers
The Complex Numbers
Ordinal Arithmetics
The Modification of a Function by a Function and the Iteration of the
Composition of a Function
Finite Sequences and Tuples of Elements of a Non-empty Set
Curried and Uncurried Functions
Cardinal Arithmetics
Fano-Desargues Parallelity Spaces
Real Function Spaces
Tarski's Classes and Ranks
Non-contiguous Substrings and One-to-one Finite Sequences
Pigeon Hole Principle
Linear Combinations in Real Linear Space
Koenig's Theorem
Universal Classes
Analytical Ordered Affine Spaces
Metric Spaces
Ordered Affine Spaces Defined in Terms of Directed Parallelity - part I
Parallelity and Lines in Affine Spaces
Volume 1(4)
Classical Configurations in Affine Planes
Affine Localizations of Desargues Axiom
Binary Operations Applied to Finite Sequences
Semigroup Operations on Finite Sequences
The Collinearity Structure
The Sum and Product of Finite Sequences of Real Numbers
A Classical First Order Language
Classical and Non-classical Pasch Configurations in Ordered Affine Planes
The Lattice of Real Numbers. The Lattice of Real Functions.
A Construction of an Abstract Space of Conguence of Vectors
A First-Order Predicate Calculus
Parital Functions from a Domain to a Domain
Partial Functions from a Domain to the Set of Real Numbers
Increasing and Continuous Ordinal Sequences
Transformations in Affine Spaces
Subcategories and Products of Categories
Many-Argument Relations
Interpretation and Satisfiability in the First Order Logic
Probability
Translations in Affine Planes
Introduction to Probability
A Construction of Analytical Projective Spaces
Projective Spaces - Part I
Topological Properties of Subsets in Real Numbers
Properties of Real Functions
Real Function Continuity
Real Function Uniform Continuity
Real Function Differentiability
Average Value Theorems for Real Functions of One Variable
Volume 1(5)
Properties of Fields
Filters -- Part I
Groups
The Divisibilty of Integers and Integer Relatively Primes
>From Loops to Abelian Multiplicative Groups with Zero
Basic Properties of Rational Numbers
Basis of Real Linear Space
Finite Sums of Vectors in Vector Space
Subgroup and Cosets of Subgroups
Subspaces and Cosets of Subspaces in Vector Space
Operations on Subspaces in Vector Space
Linear Combinations in Vector Space
Basis of Vector Space
Factorial and Newton Coefficients
Analytical Metric Affine Spaces and Planes
Projective Spaces - part II
Projective Spaces - part III
Projective Spaces - part IV
Projective Spaces - part V
Projective Spaces - part VI
Some Elementary Notions of the Theory of Petri Nets
Classes of Conjugation. Normal Subgroups
Replacing of Variables in Formulas of ZF Theory
The Reflection Theorem
Binary Operations on Finite Sequences
Finite Join and Finite Meet, and Dual Lattices
Consequences of the Reflection Theorem
Volume 2(1)
Construction of Rings and Left-, Right-, and Bi-Modules over a Ring
Desargues Theorem in Projective 3-Space
The Limit of a Real Function at Infinity
One-Side Limits of a Real Function at a Point
Lattice of Subgroups of a Group, Frattini Subgroup
Equalities and Inequalities in Real Numbers
Countable Sets and Hessenberg's Theorem
The Limit of a Real Function at a Point
The Limit of a Composition of Real Functions
Locally Connected Spaces
Construction of Finite Sequences over Ring, and Left-, Right, and
Bi-Modules over a Ring
Relations of Tolerance
Real Normed Space
Schemes of Existence of Some Types of Functions
Integer and Rational Exponents
Homothetics and Shears in Affine Planes
Directed Geometrical Bundles and Their Analytical Representation
Definable Functions
Propositional Calculus
Complex Spaces
Several Properties of Fields. Field Theory.
Infimum and Supremum of the Set of Real Numbers, Measure Theory
Series of Positive Real Numbers, Measure Theory
>From Double Loops to Fields
Voluem 2(2)
Metrics in Cartesian Product
Submetric Spaces - part I
On Pseudometric Spaces
Real Exponents and Logarithms
Hessenberg Theorem
Three-Argument Operations and Four-Argument Operations
Incidence Projective Spaces
One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation
Algebra of Normal Forms
Ordered Rings - part I
Ordered Rings - part II
Ordered Rings - part III
N-Tuples and Cartesian Products for n=5
Ternary Fields
The sigma-additive Measure Theory
Incidence Projective Space (a reduction theorem in a plane)
Groups, Rings, Left- and Right-Modules
Finite Sums of Vectors in Left Module over Associative Ring
Submodules and Cosets of Submodules in Left Module over
Associative Ring
Operations on Submodules in Left Module over Associative Ring
Linear Combinations in Left Module over Associative Ring
Lienar Independence in Left Module over Domain
Calculus of Propositions
Calculus of Quantifiers, Deduction Theorem
Volume 2(3)
A Construction of Analytical Ordered Trapezium Spaces
On Projections in Projective Planes, Part II
Metric-Affine Configurations in Metric Affine Planes - Part I
Metric-Affine Configurations in Metric Affine Planes - Part II
Fanoian, Pappian and Desarguesian Affine Spaces
Elementary Variants of Affine Configuration Theorems
Semi-Affine Space
Planes in Affine Spaces
Graphs
Mostowski's Fundamental Operations - part I
A Projective Closure and Projective Horizon of an Affine Space
Schemes
Algebra of Normal Forms Is a Heyting Algebra
Koenig's Lemma
Monotonic and Continuous Real Function
Real Function Differentiability - Part II
Preliminaries to the Lambek Calculus
Oppositie Categories and Contravariant Functors
Mostowski's Fundamental Operations - Part II
Fundamental Types of Metric Affine Spaces
Filters - Part II. Quotient Lattices Module Filters and Direct Product
of Two Lattices
Shear Theorems and Their Role in Affine Geometry
Volume 2(4)
Series
The Lattice of Natural Numbers and the Sublattice of it. The
Set of Prime Numbers
Commutator and Center of a Group
Natural Transformations. Discrete Categories
Matrices. Abelian Group of Matrices.
Paracompact and Metrizable Spaces
Atlas of Midpoint Algebra
Several Properties of the sigma-additive Measure
Metrics in the Cartesian Product - Part II
Fix Point Theorem for Compact Spaces
Quadratic Inequalities
Introduction to Banach and Hilbert Spaces - Part I
Introduction to Banach and Hilbert Spaces - Part II
Introduction to Banach and Hilbert Spaces - Part III
Category Ens
A Borsuk Theorem on Homotopy Types
Cartesian Product of Functions
Introduction to Modal Propositional Logic
Totally Bounded Metric Spaces
Categories of Groups
Homomorphisms and Isomorphisms of Groups. Quotient Group
Rings and Modules -- Part II
Free Modules
Oriented Metric-Affine Plane - Part I
The Euclidean Space
Metric Spaces as Topological Spaces - Fundamental Concepts
Heine-Borel's Covering Theorem
Some Facts about Union of Two Functions and Continuity of
Union of Functions
Volume 2(5)
The Topological Space E^2_T. Arcs, Line Segments and Special
Polygonal Arcs
Cyclic Groups and Some of Their Properties - Part I
Isomorphisms of Categories
Similarity of Formulae
Category of Rings
Category of Left Modules
Real Function One-Side Differentiability
Sequences in Metric Spaces
The Topological Sapce E^2_T. Simple Closed Curves.
Separated and Weakly Separated Subspaces of Topological Spaces
The de l'Hopital Theorem
Comma Category
Context-Free Grammar - Part I
Completeness of the sigma-additive Measure. Measure Theory.
Series in Banach and Hilbert Spaces
Products and Coproducts in Categories
Transpose Matrices and Groups of Permutations
Complete Lattices
Voluem 3(1)
Continuity of Mappings Over the Union of Subspaces
Functional Sequences from a Domain to a Domain
Reper Algebras
Isomorphisms of Cyclic Groups, Some Properties of Cyclic Groups
Some Isomorphisms Between Functor Categories
The Lattice of Domains of a Topological Space
Submodules
Oriented Matric-Affine Plane - Part II
Opposite Rings, Modules and their Morphisms
Properties of Caratheodor's Measure
Completeness of the Lattices of Domains of a Topological Space
On Paracompactness of Metrizable Spaces
The Brouwer Fixed Point Theorem for Intervals
On Powers of Cardinals
Basic Properties of Connecting Points with Line Segments in E^2_T
Connectedness Conditions Using Polygonal Arcs
Introduction to Go-Board Part I
Introduction to Go-Board Part II
Introduction to Go-Board Part III
Go-Board Theorem
Some Properties of Binary Relations
Volume 3(2)
The Jordan Property for Certain Subsets of the Plane
The Lattice of Domains of an Extremally Disconnected Space
A Mathematical Model of a CPU
Cartesian Categories
Algebgra of Vector Functions
On a Duality Between Weakly Separated Subspaces of Topological Spaces
Basic Petri Net Concepts
Finite Topological Spaces
Sets and Functions of Trees and Joining Operations of Trees
Sum and Product of Finite Sequences of Elements of a Field
Monoids
Monoid of Multisets and Subsets
Product of Families of Groups and Vector Spaces
On a Mathematical Model of Programs
Basic Notation of Universal Algebra
Coherent Space
Properties of the Intervals of Real Numbers
Subspaces of Real Linear Space Generated by One, Two, or Three
Vectors and Their Cosets
Functions and Finite Sequences of Real Numbers
Properties of Partial Functions from a Domain to the Set of Real
Numbers
Domains of Submodules, Join and Meet of Finite Sequences of Submodules
and Quotient Modules
Remarks on Special Subsets of Topological Spaces
On Discrete and Almost Discrete Topological Spaces
Adam Lecko
Agata Darmochwal
Alicia de La Cruz
Andrezej Kondracki
Andrezej Nedzusiak
Andrezej Trybulec
Andrezej Nedzusiak
Anna Lango
Anna Zalewska
Barbara Konstanta
Beata Madras
Beata Padlewska
Beata Perkowska
Bialas Jozef
Bogdan Nowak
Czeslaw Bylinski
Dariusz Surowik
Elzbieta Kraszewska
Edmunb Woronowicz
Ewa Burakowska
Eugeniusz Kusak
Grzegorz Bancerek
Grzegorz Lewandowski
Grzegorz Zwara
Halina Swieczkowska
Henryk Oryszczyszyn
Hiroshi Imura
Hiroshi Yamazaki
Jan Popiolek
Jan Stankiewicz
Jaroslaw Kotowicz
Jaroslaw Zajkowski
Jolanta Swierzynska
Jozef Bialas
Katarzyna Jankowska
Konrad Raczkowski
Krzysztof Hryniewiecki
Krzysztof Prazmowski
Krzysztof Radziszewski
Leszek Borys
Malgorzata Korolkiewicz
Marek Chmur
Mariusz Startek
Masayoshi Eguchi
Michal Muzalewski
Michal J. Trybulec
Miroslaw Wysocki
Pauline Kawamoto
Patricia Carlson
Pawel Sadowski
Piotr Rudnicki
Rafal Kwiatek
Slawomir Bialecki
Stanislaw Czuba
Stanislaw Kanas
Stanislaw Zukowski
Toshihiko Watanabe
Waldemar Korczynski
Wojciech A. Trybulec
Wojciech Leonczuk
Wojciech Skaba
Wojciech Zielonka
Yasunari Shidama
Yatsuka Nakamura
Yuji Sakai
Zinaida Trybulec
Zbigniew Karno