Mizar articles

• abcmiz_0: On semilattice structure of {M}izar types
• abcmiz_1: Towards the construction of a model of Mizar concepts
• abcmiz_a: A Model of Mizar Concepts -- Unification
• abian: Abian's Fixed Point Theorem
• absred_0: Abstract Reduction Systems and Idea of {K}nuth {B}endix Completion Algorithm
• absvalue: Some Properties of Functions Modul and Signum
• aescip_1: Formalization of the Advanced Encryption Standard -- Part {I}
• aff_1: Parallelity and Lines in Affine Spaces
• aff_2: Classical Configurations in Affine Planes
• aff_3: Affine Localizations of Desargues Axiom
• aff_4: Planes in Affine Spaces
• afinsq_1: Zero Based Finite Sequences
• afinsq_2: Basic Properties and Concept of Selected Subsequence of Zero Based Finite Sequences
• afproj: A Projective Closure and Projective Horizon of an Affine Space
• afvect0: Directed Geometrical Bundles and Their Analytical Representation
• afvect01: One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation
• aimloop: {AIM } Loops and the {AIM } Conjecture
• alg_1: Homomorphisms of algebras. Quotient Universal Algebra
• algnum_1: Algebraic Numbers
• algseq_1: Construction of Finite Sequences over Ring and Left-, Right-, and Bi-Modules over a Ring
• algspec1: Technical Preliminaries to Algebraic Specifications
• algstr_0: Basic Algebraic Structures
• algstr_1: From Loops to Abelian Multiplicative Groups with Zero
• algstr_2: From Double Loops to Fields
• algstr_3: Ternary Fields
• algstr_4: Free Magmas
• ali2: Fix Point Theorem for Compact Spaces
• altcat_1: Categories without Uniqueness of { \bf cod } and { \bf dom }
• altcat_2: Examples of Category Structures. Subcategories
• altcat_3: Basic properties of objects and morphisms. In categories without uniqueness of { \bf cod } and { \bf dom }
• altcat_4: On the Categories Without Uniqueness of { \bf cod } and { \bf dom } . Some Properties of the Morphisms and the Functors
• altcat_5: Products in Categories without Uniqueness of { \bf cod } and { \bf dom }
• altcat_6: Coproducts in Categories without Uniqueness of { \bf cod } and { \bf dom}
• ami_2: On a Mathematical Model of Programs
• ami_3: Some Remarks on Simple Concrete Model of Computer
• ami_4: Euclid's Algorithm
• ami_5: On the Decomposition of the States of SCM
• ami_6: On the Instructions of { \bf SCM }
• ami_wstd: Weakly Standard Ordering of Instruction Locations
• amistd_1: Standard Ordering of Instruction Locations
• amistd_2: On the Composition of Macro Instructions of Standard Computers
• amistd_3: A Tree of Execution of a Macroinstruction
• amistd_4: Input and Output of Instructions
• amistd_5: Relocable Instructions
• analmetr: Analytical Metric Affine Spaces and Planes
• analoaf: Analytical Ordered Affine Spaces
• analort: Oriented Metric-Affine Plane - Part I
• anproj10: {C}ross-ratio in Real Vector Space
• anproj11: Principle of Duality in Real Projective Plane: a Proof of the Converse of {D}esargues' Theorem and a Proof of the Converse of {P}appus' Theorem by Transport
• anproj_1: A Construction of Analytical Projective Space
• anproj_2: Projective Spaces
• anproj_8: Homography in $\mathbbRP^2$
• anproj_9: Group of Homography in Real Projective Plane
• aofa_000: Mizar Analysis of Algorithms: Preliminaries
• aofa_a00: Program Algebra over an Algebra
• aofa_a01: Analysis of Algorithms: An Example of a Sort Algorithm
• aofa_i00: Mizar Analysis of Algorithms: Algorithms over Integers
• aofa_l00: Algebraic Approach to Algorithmic Logic
• arithm: Field Properties of Complex Numbers - Requirements
• armstrng: Armstrong's Axioms
• arrow: Arrow's Impossibility Theorem
• arytm_0: Introduction to Arithmetics
• arytm_1: Non negative real numbers. Part II
• arytm_2: Non negative real numbers. Part I
• arytm_3: Arithmetic of Non Negative Rational Numbers
• ascoli: Ascoli-Arzela's Theorem
• asympt_0: Asymptotic notation. Part I: Theory
• asympt_1: Asymptotic notation. Part II: Examples and Problems
• asympt_2: Polynomially Bounded Sequences and Polynomial Sequences
• asympt_3: Algebra of Polynomially Bounded Sequences and Negligible Functions
• autalg_1: On the Group of Automorphisms of Universal Algebra & Many Sorted Algebra
• autgroup: On the Group of Inner Automorphisms
• axioms: Strong arithmetic of real numbers
• bagord_2: On Multiset Ordering
• bagorder: On Ordering of Bags
• ballot_1: Bertrand's Ballot Theorem
• basel_1: Basel Problem -- Preliminaries
• basel_2: Basel Problem
• bcialg_1: Several Classes of {BCI}-algebras and Their Properties
• bcialg_2: Congruences and Quotient Algebras of {BCI}-algebras
• bcialg_3: Several Classes of {BCK}-algebras and Their Properties
• bcialg_4: BCI-Algebras with Condition (S) and Their Properties
• bcialg_5: General Theory of Quasi-Commutative BCI-algebras
• bcialg_6: {BCI}-Homomorphisms
• bciideal: Ideals of BCI-Algebras and Their Properties
• bhsp_1: Introduction to Banach and Hilbert spaces - Part I
• bhsp_2: Introduction to Banach and Hilbert spaces - Part II
• bhsp_3: Introduction to Banach and Hilbert spaces - Part III
• bhsp_4: Series in Banach and Hilbert Spaces
• bhsp_5: Bessel's Inequality
• bhsp_6: On Some Properties of Real {H}ilbert Space, {I}
• bhsp_7: On Some Properties of Real {H}ilbert Space, {II}
• bilinear: Bilinear Functionals in Vector Spaces
• binari_2: Binary Arithmetics. Addition and Subtraction of Integers
• binari_3: Binary Arithmetics. Binary Sequences
• binari_4: A Representation of Integers by Binary Arithmetics and Addition of Integers
• binari_6: Binary Representation of Natural Numbers
• binarith: Binary Arithmetics. Addition
• binom: The Binomial Theorem for Algebraic Structures
• binop_1: Binary Operations
• binop_2: Binary Operations on Numbers
• binpack1: Algorithm NextFit for the Bin Packing Problem
• bintree1: On Defining Functions on Binary Trees
• bintree2: Full Trees
• birkhoff: Birkhoff Theorem for Many Sorted Algebras
• bkmodel1: Beltrami-Klein Model, {P}art {I}
• bkmodel2: Beltrami-Klein model, Part {II}
• bkmodel3: Beltrami-Klein model, Part {III}
• bkmodel4: Beltrami-Klein model, Part {IV}
• boole: Boolean Properties of Sets - Requirements
• boolealg: Boolean Properties of Lattices
• boolmark: Basic Concepts for Petri Nets with Boolean Markings. Boolean Markings and the Firability/Firing of Transitions
• bor_cant: Borel-Cantelli Lemma
• borsuk_1: A Borsuk Theorem on Homotopy Types
• borsuk_2: Introduction to Homotopy Theory
• borsuk_3: Properties of the Product of Compact Topological Spaces
• borsuk_4: On the Decompositions of Intervals and Simple Closed Curves
• borsuk_5: On the Subcontinua of a Real Line
• borsuk_6: Algebraic Properties of Homotopies
• borsuk_7: The {B}orsuk-Ulam Theorem
• brouwer: Brouwer Fixed Point Theorem for Disks on the Plane
• brouwer2: Brouwer Fixed Point Theorem in the General Case
• brouwer3: Brouwer Invariance of Domain Theorem
• bspace: The Vector Space of Subsets of a Set Based on Symmetric Difference
• bvfunc11: Predicate Calculus for Boolean Valued Functions, III
• bvfunc14: Predicate Calculus for Boolean Valued Functions, { VI }
• bvfunc25: Propositional Calculus for Boolean Valued Functions, {VII}
• bvfunc_1: A Theory of Boolean Valued Functions and Partitions
• bvfunc_2: A Theory of Boolean Valued Functions and Quantifiers with Respect to Partitions
• bvfunc_3: Predicate Calculus for Boolean Valued Functions, { I }
• bvfunc_4: Predicate Calculus for Boolean Valued Functions, II
• bvfunc_5: Propositional Calculus for Boolean Valued Functions, I
• bvfunc_6: Propositional Calculus for Boolean Valued Functions, II
• c0sp1: Banach Algebra of Bounded Functionals
• c0sp2: Banach Algebra of Continuous Functionals and Space of Real-valued Continuous Functionals with Bounded Support
• c0sp3: Functional Space Consisted by Continuous Functions on Topological Space
• calcul_1: A Sequent Calculus for First-Order Logic
• calcul_2: Consequences of the Sequent Calculus
• cantor_1: The Cantor Set
• card_1: Cardinal Numbers
• card_2: Cardinal Arithmetics
• card_3: K\"onig's Theorem
• card_4: Countable Sets and Hessenberg's Theorem
• card_5: On Powers of Cardinals
• card_fil: Basic facts about inaccessible and measurable cardinals
• card_fin: Cardinal Numbers and Finite Sets
• card_lar: Mahlo and inaccessible cardinals
• cardfil2: Convergent Filter Bases
• cardfil3: Summable Family in a Commutative Group
• cardfil4: Double Sequences and Iterated Limits in Regular Space
• cardfin2: Counting Derangements, Counting Non Bijective Functions and the Birthday Problem
• cat_1: Introduction to Categories and Functors
• cat_2: Subcategories and Products of Categories
• cat_3: Products and Coproducts in Categories
• cat_4: Cartesian Categories
• cat_5: Categorial Categories and Slice Categories
• cat_6: Object-Free Definition of Categories
• cat_7: Categorical Pullbacks
• cat_8: Exponential Objects
• catalan1: Catalan Numbers
• catalan2: The {C}atalan Numbers. {P}art {II}
• catalg_1: Algebra of Morphisms
• cayldick: Cayley-Dickson Construction
• cayley: Cayley's Theorem
• cc0sp1: Banach Algebra of Bounded Complex-Valued Functionals
• cc0sp2: Banach Algebra of Complex-Valued Continuous Functionals and Space of Complex-valued Continuous Functionals with Bounded Support
• cfcont_1: Property of Complex Sequence and Continuity of Complex Function
• cfdiff_1: Complex Function Differentiability
• cfdiff_2: Cauchy-Riemann Differential Equations of Complex Functions
• cfuncdom: Complex Valued Function's Space
• cfunct_1: Property of Complex Functions
• cgames_1: Conway's Games and Some of Their Basic Properties
• chain_1: Chains on a Grating in Euclidean Space
• chord: Chordal Graphs
• circcmb2: Combining of Multi Cell Circuits
• circcmb3: Preliminaries to Automatic Generation of Mizar Documentation for Circuits
• circcomb: Combining of Circuits
• circled1: Circled Sets, Circled Hull, and Circled Family
• circtrm1: Circuit Generated by Terms and Circuit Calculating Terms
• circuit1: Introduction to Circuits, I
• circuit2: Introduction to Circuits, II
• ckspace1: The $C^k$ Space
• classes1: Tarski's Classes and Ranks
• classes2: Universal Classes
• classes3: Grothendieck Universes
• clopban1: Complex {B}anach Space of Bounded Linear Operators
• clopban2: Banach Algebra of Bounded Complex Linear Operators
• clopban3: Series on Complex {B}anach Algebra
• clopban4: Exponential Function on Complex {B}anach Algebra
• closure1: On the Many Sorted Closure Operator and the Many Sorted Closure System
• closure2: On the Closure Operator and the Closure System of Many Sorted Sets
• closure3: Algebraic Operation on Subsets of Many Sorted Sets
• clvect_1: Complex Linear Space and Complex Normed Space
• clvect_2: Convergent Sequences in Complex Unitary Space
• clvect_3: Cauchy Sequence of Complex Unitary Space
• coh_sp: Coherent Space
• cohsp_1: Continuous, Stable, and Linear Maps of Coherence Spaces
• collsp: The Collinearity Structure
• combgras: Combinatorial {G}rassmannians
• commacat: Comma Category
• compact1: Alexandroff One Point Compactification
• compl_sp: Complete Spaces
• complex1: The Complex Numbers
• complex2: Inner Products and Angles of Complex Numbers
• complex3: Multiplication-related Classes of Complex Numbers
• complfld: The Field of Complex Numbers
• complsp1: Complex Spaces
• complsp2: The Inner Product and Conjugate of Finite Sequences of Complex Numbers
• compos_0: Commands Structure
• compos_1: Composition of Machines, Instructions and Programs
• compos_2: The Elementary Macroinstructions
• comptrig: Trigonometric Form of Complex Numbers
• compts_1: Compact Spaces
• comput_1: The set of primitive recursive functions
• comseq_1: Complex Sequences
• comseq_2: Conjugate Sequences, Bounded Complex Sequences and Convergent Complex Sequences
• comseq_3: Convergence and the Limit of Complex Sequences. Series
• conaffm: Metric-Affine Configurations in Metric Affine Planes - Part I
• conlat_1: Introduction to Concept Lattices
• conlat_2: A Characterization of Concept Lattices; Dual Concept Lattices
• conmetr: Metric-Affine Configurations in Metric Affine Planes - Part II
• conmetr1: Shear Theorems and Their Role in Affine Geometry
• connsp_1: Connected Spaces
• connsp_2: Locally Connected Spaces
• connsp_3: Components and Unions of Components
• convex1: Convex Sets and Convex Combinations
• convex2: Some Properties for Convex Combinations
• convex3: Convex Hull, Set of Convex Combinations and Convex Cone
• convex4: Convex Sets and Convex Combinations on Complex Linear Spaces
• convfun1: Definition of Convex Function and {J}ensen's Inequality
• counters: Extended Natural Numbers and Counters
• cousin: Cousin's Lemma
• cousin2: Gauge Integral
• cqc_lang: A Classical First Order Language
• cqc_sim1: Similarity of Formulae
• cqc_the1: A First-Order Predicate Calculus. Axiomatics, the Consequence Operation and a Concept of Proof
• cqc_the2: Calculus of Quantifiers. Deduction Theorem
• cqc_the3: Logical Equivalence of Formulae
• csspace: Complex Linear Space of Complex Sequences
• csspace2: Hilbert Space of Complex Sequences
• csspace3: Banach Space of Absolute Summable Complex Sequences
• csspace4: Complex Banach Space of Bounded Complex Sequences
• dblseq_1: Double Sequences and Limits
• dblseq_2: Double Series and Sums
• dblseq_3: Extended Real Valued Double Sequence and Its Convergence
• decomp_1: On the Decomposition of the Continuity
• descip_1: Formalization of the Data Encryption Standard
• dickson: Dickson's lemma
• diff_1: Difference and Difference Quotient
• diff_2: Difference and Difference Quotient -- Part {II}
• diff_3: Difference and Difference Quotient -- Part {III}
• diff_4: Difference and Difference Quotient -- Part {IV}
• dilworth: Dilworth's Decomposition Theorem for Posets
• diophan1: Introduction to {D}iophantine Approximation
• diophan2: Introduction to {D}iophantine Approximation -- Part 2
• diraf: Ordered Affine Spaces Defined in Terms of Directed Parallelity - part I
• dirort: Oriented Metric-Affine Plane - Part II
• dist_1: Probability on Finite and Discrete Set and Uniform Distribution
• dist_2: Posterior Probability on Finite Set
• domain_1: Domains and Their Cartesian Products
• dtconstr: On Defining Functions on Trees
• dualsp01: Dual Spaces and Hahn-Banach's Theorem
• dualsp02: Bidual Spaces and Reflexivity of Real Normed Spaces
• dualsp03: Weak Convergence and Weak* Convergence
• dualsp04: The Orthogonal Projection and {R}iesz Representation Theorem
• dualsp05: F. Riesz Theorem
• dynkin: Dynkin's Lemma in Measure Theory
• e_siec: Definitions of Petri Net - Part II
• ec_pf_1: Set of Points on Elliptic Curve in Projective Coordinates
• ec_pf_2: Operations of Points on Elliptic Curve in Projective Coordinates
• ec_pf_3: Operations of Points on Elliptic Curve in Affine Coordinates
• endalg: On the Monoid of Endomorphisms of Universal Algebra \& Many Sorted Algebra
• ens_1: Category Ens
• entropy1: Definition and Some Properties of Information Entropy
• enumset1: Enumerated Sets
• eqrel_1: Equivalence Relations and Classes of Abstraction
• equation: Equations in Many Sorted Algebras
• euclid: The Euclidean Space
• euclid10: Some Facts about Trigonometry and Euclidean Geometry
• euclid11: Morley's Trisector Theorem
• euclid12: Circumcenter, Circumcircle, and Centroid of a Triangle
• euclid13: Altitude, Orthocenter of a Triangle and Triangulation
• euclid_2: The Inner Product of Finite Sequences and of Points of $n$-dimensional Topological Space
• euclid_3: Angle and Triangle in {E}uclidian Topological Space
• euclid_4: Lines in $n$-Dimensional Euclidean Spaces
• euclid_5: Cross Products and Tripple Vector Products in 3-dimensional Euclidian Space
• euclid_6: Heron's Formula and Ptolemy's Theorem
• euclid_7: The Real Vector Spaces of Finite Sequences Are Finite Dimensional
• euclid_8: Vector Function and its Differentiation Formulas in 3-dimensional Euclidean Spaces
• euclid_9: The Correspondence Between $n$-dimensional {E}uclidean Space and the Product of $n$ Real Lines
• euclidlp: Lines on Planes in $n$-Dimensional Euclidean Spaces
• euclmetr: Fundamental Types of Metric Affine Spaces
• euler_1: Euler's Function
• euler_2: Euler's {T}heorem and Small {F}ermat's Theorem
• eulrpart: {E}uler's {P}artition {T}heorem
• exchsort: Sorting by Exchanging
• extens_1: Extensions of Mappings on Generator Set
• extpro_1: Externally Programmed Machines
• extreal1: Basic Properties of Extended Real Numbers
• facirc_1: Full Adder Circuit. Part { I }
• facirc_2: Full Adder Circuit. Part { II }
• fcont_1: Real Function Continuity
• fcont_2: Real Function Uniform Continuity
• fcont_3: Monotonic and Continuous Real Function
• fdiff_1: Real Function Differentiability
• fdiff_10: Several Differentiation Formulas of Special Functions -- Part {V}
• fdiff_11: Several Differentiation Formulas of Special Functions -- Part {VII}
• fdiff_2: Real Function Differentiability - Part II
• fdiff_3: Real Function One-Side Differantiability
• fdiff_4: Several Differentiable Formulas of Special Functions
• fdiff_5: Some Differentiable Formulas of Special Functions
• fdiff_6: Several Differentiable Formulas of Special Functions -- Part {II}
• fdiff_7: Several Differentiation Formulas of Special Functions -- Part {III}
• fdiff_8: Several Differentiation Formulas of Special Functions -- Part {IV}
• fdiff_9: Several Differentiation Formulas of Special Functions -- Part {V}
• ff_siec: Definitions of Petri Net - Part I
• fib_fusc: Two Programs for {\bf SCM}. Part II - Proofs
• fib_num: Fibonacci Numbers
• fib_num2: Some Properties of {F}ibonacci Numbers
• fib_num3: Lucas Numbers and Generalized {F}ibonacci Numbers
• fib_num4: Representation of the {F}ibonacci and {L}ucas Numbers in Terms of the Floor and Ceiling Functor
• field_1: On Roots of Polynomials over K[X]/<p>
• field_2: On Monomorphisms and Subfields
• field_3: On the Intersection of Fields $F$ with $F[X]$
• field_4: Field Extensions and {K}ronecker's Construction
• field_5: Renamings and a Condition-free Formalization of {K}ronecker's Construction
• field_6: Ring and Field Adjunctions, Algebraic Elements and Minimal Polynomials
• field_7: Algebraic Extensions
• field_8: Splitting Fields
• field_9: Quadratic Extensions
• filerec1: A Theory of Sequential Files
• filter_0: Filters - Part I. Implicative Lattices
• filter_1: Filters - Part II. Quotient Lattices Modulo Filters and Direct Product of Two Lattices
• filter_2: Ideals
• fin_topo: Finite Topological Spaces. Finite Topology Concepts and Neighbourhoods
• finance1: Elementary Introduction to Stochastic Finance in Discrete Time
• finance2: Events of Borel Sets, Construction of Borel Sets and Random Variables for Stochastic Finance
• finance3: Modelling Real World Using Stochastic Processes and Filtration
• finance4: Introduction to Stopping Time in Stochastic Finance Theory
• finance5: Introduction to Stopping Time in Stochastic Finance Theory: Part {II}
• finance6: Introduction to Stochastic Finance: Random-Variables and Arbitrage Theory
• finseq_1: Segments of Natural Numbers and Finite Sequences
• finseq_2: Finite Sequences and Tuples of Elements of a Non-empty Sets
• finseq_3: Non-contiguous Substrings and One-to-one Finite Sequences
• finseq_4: Pigeon Hole Principle
• finseq_5: Some Properties of Restrictions of Finite Sequences
• finseq_6: On the Decomposition of Finite Sequences
• finseq_7: On Replace Function and Swap Function for Finite Sequences
• finseq_8: Concatenation of Finite Sequences Reducing Overlapping Part and an Argument of Separators of Sequential Files
• finseq_9: Arithmetic Operations on Short Finite Sequences
• finseqop: Binary Operations Applied to Finite Sequences
• finset_1: Finite Sets
• finsop_1: Binary Operations on Finite Sequences
• finsub_1: Boolean Domains
• fintopo2: Formal topological spaces
• fintopo3: Some Set Series in Finite Topological Spaces. {F}undamental Concepts for Image Processing
• fintopo4: Continuous Mappings between Finite and One-Dimensional Finite Topological Spaces
• fintopo5: Homeomorphism between Finite Topological Spaces, Two-Dimensional Lattice Spaces and a Fixed Point Theorem
• fintopo6: Connectedness and Continuous Sequences in Finite Topological Spaces
• fintopo7: Topology from Neighbourhoods
• fintopo8: A Case Study of Transport Urysohn's Lemma from TopSpace Defined with Open Sets to TopSpace Defined with Neighborhoods
• flang_1: Formal Languages -- Concatenation and Closure
• flang_2: Regular Expression Quantifiers -- $m$ to $n$ Occurrences
• flang_3: Regular Expression Quantifiers -- at least $m$ Occurrences
• flexary1: Flexary Operations
• fomodel0: Preliminaries to Classical First-order Model Theory
• fomodel1: Definition of first order language with arbitrary alphabet. Syntax of terms, atomic formulas and their subterms
• fomodel2: First order languages: syntax, part two; semantics
• fomodel3: Free interpretation, quotient interpretation and substitution of a letter with a term for first order languages
• fomodel4: Sequent calculus, derivability, provability. Goedel's completeness theorem
• fraenkel: Function Domains and Fr{\ae}nkel Operator
• frechet: First-countable, Sequential, and { F } rechet Spaces
• frechet2: The Sequential Closure Operator In Sequential and Frechet Spaces
• freealg: Free Universal Algebra Construction
• friends1: The Friendship Theorem
• fscirc_1: Full Subtracter Circuit. Part { I }
• fscirc_2: Full Subtracter Circuit. Part {II}
• fsm_1: Minimization of finite state machines
• fsm_2: On state machines of calculating type
• fsm_3: Equivalence of Epsilon, Nondeterministic [Finite] Automata and Deterministic [Finite] Automata
• ftacell1: Stability of the 4-2 Binary Addition Circuit Cells. Part {I}
• funcop_1: Binary Operations Applied to Functions
• funcsdom: Real Functions Spaces
• funct_1: Functions and Their Basic Properties
• funct_2: Functions from a Set to a Set
• funct_3: Basic Functions and Operations on Functions
• funct_4: The Modification of a Function by a Function and the Iteration of the Composition of a Function
• funct_5: Curried and Uncurried Functions
• funct_6: Cartesian Product of Functions
• funct_7: Miscellaneous Facts about Functions
• funct_8: Basic properties of even and odd functions
• funct_9: Basic Properties of Periodic Functions
• functor0: Functors for Alternative Categories
• functor1: Basic Properties of Functor Structures
• functor2: Category of Functors between Alternative Categories
• functor3: The Composition of Functors and Transformations in Alternative Categories
• fuzimpl1: Formal Introduction to Fuzzy Implications
• fuzimpl2: Fundamental Properties of Fuzzy Implications
• fuzimpl3: On Fuzzy Negations Generated by Fuzzy Implications
• fuznorm1: Basic Formal Properties of Triangular Norms and Conorms
• fuznum_1: The Formal Construction of Fuzzy Numbers
• fuzzy_1: Concept of Fuzzy Set and Membership Function and Basic Properties of Fuzzy Set Operation
• fuzzy_2: Basic Properties of Fuzzy Set Operation and Membership Function
• fuzzy_4: Properties of Fuzzy Relation
• fuzzy_5: Some Properties of Membership Functions Composed of Triangle Functions and Piecewise Linear Functions
• fvaluat1: Valuation Theory, Part {I}
• fvsum_1: Sum and Product of Finite Sequences of Elements of a Field
• gate_1: Logic Gates and Logical Equivalence of Adders
• gate_2: Correctness of Binary Counter Circuits
• gate_3: Correctness of Johnson Counter Circuits
• gate_4: Correctness of a Cyclic Redundancy Check Code Generator
• gate_5: Correctness of the High Speed Array Multiplier Circuits
• gaussint: Gaussian Integers
• gcd_1: The correctness of the Generic Algorithms of Brown and Henrici concerning Addition and Multiplication in Fraction Fields
• genealg1: Basic Properties of Genetic Algorithm
• geomtrap: A Construction of Analytical Ordered Trapezium Spaces
• gfacirc1: Generalized Full Adder Circuits (GFAs). {P}art {I}
• gfacirc2: Stability of n-bit Generalized Full Adder Circuits (GFAs). Part {II}
• glib_000: Alternative Graph Structures
• glib_001: Walks in a Graph
• glib_002: Trees: Connected, Acyclic Graphs
• glib_003: Weighted and Labeled Graphs
• glib_004: Proof of Dijkstra's Shortest Path Algorithm & Prim's Minimum Spanning Tree Algorithm
• glib_005: Proof of Ford/Fulkerson's Maximum Network Flow Algorithm
• glib_006: About Supergraphs, Part {I}
• glib_007: About Supergraphs, Part {II}
• glib_008: About Supergraphs, {P}art {III}
• glib_009: Underlying Simple Graphs
• glib_010: About Graph Mappings
• glib_011: About Graph Mappings
• glib_012: About Graph Complements
• glib_013: Refined Finiteness and Degree properties in Graphs
• glib_014: About Graph Unions and Intersections
• glib_015: About Graph Sums
• glibpre0: Miscellaneous Graph Preliminaries
• glibpre1: Miscellaneous Graph Preliminaries, {I}
• glunir00: Unification of Graphs and Relations in {M}izar
• goboard1: Introduction to Go-Board - Part I. Basic Notations
• goboard2: Introduction to Go-Board - Part II. Go-Board Determined by Finite Sequence of point from ${\calE}^2_{\rm T}$
• goboard3: Properties of Go-Board - Part III
• goboard4: Go-Board Theorem
• goboard5: Decomposing a Go Board into Cells
• goboard6: On the Geometry of a Go-board
• goboard7: On the Go Board of a Standard Special Circular Sequence
• goboard8: More on Segments on a Go Board
• goboard9: Left and Right Component of the Complement of a Special Closed Curve
• gobrd10: Adjacency Concept for Pairs of Natural Numbers
• gobrd11: Some Topological Properties of Cells in $R^2$
• gobrd12: The First Part of Jordan's Theorem for Special Polygons
• gobrd13: Some Properties of Cells on Go Board
• gobrd14: Properties of Left-, and Right Components
• goedcpuc: The G\"odel Completeness Theorem for Uncountable Languages
• goedelcp: G{\"o}del's Completeness Theorem
• gr_cy_1: Cyclic Groups and Some of Their Properties - Part I
• gr_cy_2: Isomorphisms of Cyclic Groups. Some Properties of Cyclic Groups
• gr_cy_3: Properties of Primes and Multiplicative Group of a Field
• graph_1: Graphs
• graph_2: Vertex sequences induced by chains
• graph_3: Euler circuits and paths
• graph_3a: A Note on the Seven Bridges of K\"onigsberg Problem
• graph_4: Oriented Simple Chains Included in Oriented Chains
• graph_5: The Underlying Principle of {D}ijkstra's Shortest Path Algorithm
• graphsp: Dijkstra's Shortest Path Algorithm
• grcat_1: Categories of Groups
• grfunc_1: Graphs of Functions
• grnilp_1: Nilpotent Groups
• groeb_1: Characterization and Existence of {G}r\"obner Bases
• groeb_2: Construction of {G}r\"obner bases. S-Polynomials and Standard Representations
• groeb_3: Construction of {G}r\"obner Bases: Avoiding S-Polynomials -- Buchberger's First Criterium
• group_1: Groups
• group_10: The Sylow Theorems
• group_11: On Rough Subgroup of a Group
• group_12: Normal Subgroup of Product of Groups
• group_14: Isomorphisms of Direct Products of Finite Cyclic Groups
• group_17: Isomorphisms of Direct Products of Finite Commutative Groups
• group_18: Isomorphisms of Direct Products of Cyclic Groups of Prime-power Order
• group_19: Definition and Properties of Direct Sum Decomposition of Groups
• group_1a: Groups -- Additive Notation
• group_2: Subgroup and Cosets of Subgroups. Lagrange theorem
• group_20: Equivalent Expressions of Direct Sum Decomposition of Groups
• group_21: Conservation Rules of Direct Sum Decomposition of Groups
• group_3: Classes of Conjugation. Normal Subgroups
• group_4: Lattice of Subgroups of a Group. Frattini Subgroup
• group_5: Commutator and Center of a Group
• group_6: Homomorphisms and Isomorphisms of Groups. Quotient Group
• group_7: The Product of the Families of the Groups
• group_8: Properties of Groups
• group_9: The {J}ordan-H\"older Theorem
• groupp_1: Some Properties of $p$-Groups and Commutative $p$-Groups
• grsolv_1: Solvable Groups
• grzlog_1: Grzegorczyk's Logics, Part 1
• gtarski1: Tarski Geometry Axioms
• gtarski2: Tarski Geometry Axioms -- Part {II}
• gtarski3: {T}arski Geometry Axioms -- Part {III}
• gtarski4: Tarski Geometry Axioms. {P}art {IV } -- Right angle
• hahnban: Hahn Banach Theorem
• hahnban1: Hahn Banach Theorem in the Vector Space over the Field of Complex Numbers
• hallmar1: The {H}all {M}arriage {T}heorem
• hausdorf: On the {H}ausdorff Distance Between Compact Subsets
• heine: Heine--Borel's Covering Theorem
• helly: Helly property for subtrees
• henmodel: Equivalences of Inconsistency and {H}enkin Models
• hermitan: Hermitan Functionals. {C}anonical Construction of Scalar Product in Quotient Vector Space
• hessenbe: Hessenberg Theorem
• heyting1: Algebra of Normal Forms Is a Heyting Algebra
• heyting2: Lattice of Substitutions Is a Heyting Algebra
• heyting3: The Incompleteness of the Lattice of Substitutions
• hfdiff_1: Several Higher Differentiation Formulas of Special Functions
• hidden: Built-in Concepts
• hilb10_1: The {M}atiyasevich Theorem -- Preliminaries
• hilb10_2: Diophantine sets -- Preliminaries
• hilb10_3: Basic Diophantine Relations
• hilb10_4: Diophantine Sets -- Preliminaries
• hilb10_5: Formalization of the {MRDP } Theorem in the {M}izar System
• hilb10_6: Prime Representing Polynomial
• hilbasis: Hilbert Basis Theorem
• hilbert1: Hilbert Positive Propositional Calculus
• hilbert2: Defining by structural induction in the positive propositional language
• hilbert3: The canonical formulae
• hilbert4: Pseudo-canonical Formulae are Classical
• holder_1: H\"older's Inequality and {M}inkowski's Inequality
• homothet: Homotheties and Shears in Affine Planes
• huffman1: Constructing Binary {H}uffman Tree
• hurwitz: Schur's Theorem on the Stability of Networks
• hurwitz2: A Test for the Stability of Networks
• idea_1: Algebraic group on Fixed-length bit integer and its adaptation to {IDEA} Cryptography
• ideal_1: Ring Ideals
• ideal_2: On Primary Ideals. {P}art {I}
• incproj: Incidence Projective Spaces
• incsp_1: Axioms of Incidence
• index_1: Indexed Category
• instalg1: Institution of Many-sorted Algebras, Part { I } : Signature Reduct of an Algebra
• int_1: Integers
• int_2: The Divisibility of Integers and Integer Relatively Primes
• int_3: The Ring of Integers, Euclidean Rings and Modulo Integers
• int_4: Linear Congruence Relation and Complete Residue Systems
• int_5: Gauss Lemma and Law of Quadratic Reciprocity
• int_6: Modular Integer Arithmetic
• int_7: Uniqueness of factoring an integer and multiplicative group $Z/pZ^{*}$
• int_8: Basic Properties of Primitive Root and Order Function
• integr10: Extended {R}iemann Integral of Functions of Real Variable and One-sided {L}aplace Transform
• integr11: Several Integrability Formulas of Special Functions -- Part {II}
• integr12: Integrability Formulas -- Part {I}
• integr13: Integrability Formulas -- Part {II}
• integr14: Integrability Formulas -- Part {III}
• integr15: Riemann Integral of Functions $\mathbbbR$ into $\mathbbbR^n$
• integr16: Riemann Integral of Functions $\mathbbbR$ into $\mathbbbC$
• integr18: Riemann Integral of Functions from $\mathbbbR$ into Real Normed Space
• integr19: Riemann Integral of Functions from $\mathbbbR$ into $n$-dimensional Real Normed Space
• integr1c: Complex Integral
• integr20: Riemann Integral of Functions from $\mathbbbR$ into Real {B}anach Space
• integr21: The Linearity of Riemann Integral on Functions from $\mathbbbR$ into Real {B}anach Space
• integr22: Riemann-Stieltjes Integral
• integr23: The Basic Existence Theorem of Riemann-Stieltjes Integral
• integr24: Improper Integral, Part {I}
• integr25: Improper Integral, Part {II}
• integra1: The Definition of Riemann Definite Integral and some Related Lemmas
• integra2: Scalar Multiple of Riemann Definite Integral
• integra3: Darboux's Theorem
• integra4: Integrability of Bounded Total Functions
• integra5: Definition of Integrability for Partial Functions from REAL to REAL and Integrability for Continuous Functions
• integra6: Integrability and the Integral of Partial Functions from $\Bbb R$ into $\Bbb R$
• integra7: Riemann Indefinite Integral of Functions of Real Variable
• integra8: Several Integrability Formulas of Special Functions
• integra9: Several Integrability Formulas of Some Functions, Orthogonal Polynomials and Norm Functions
• interva1: On the Lattice of Intervals and Rough Sets
• intpro_1: Intuitionistic Propositional Calculus in the Extended Framework with Modal Operator, Part I
• irrat_1: Irrationality of e
• isocat_1: Isomorphisms of Categories
• isocat_2: Some Isomorphisms Between Functor Categories
• isomichi: The Properties of Supercondensed Sets, Subcondensed Sets and Condensed Sets
• jct_misc: Miscellaneous { I }
• jgraph_1: Graph Theoretical Properties of Arcs in the Plane and Fashoda Meet Theorem
• jgraph_2: On Outside Fashoda Meet Theorem
• jgraph_3: On the Simple Closed Curve Property of the Circle and the Fashoda Meet Theorem for It
• jgraph_4: Fan Homeomorphisms in the Plane
• jgraph_5: General {F}ashoda {M}eet {T}heorem for Unit Circle
• jgraph_6: General {F}ashoda Meet Theorem for Unit Circle and Square
• jgraph_7: Fashoda Meet Theorem for Rectangles
• jgraph_8: The {F}ashoda Meet Theorem for Continuous Mappings
• jordan: Jordan Curve Theorem
• jordan1: The Jordan's Property for Certain Subsets of the Plane
• jordan10: Properties of the External Approximation of Jordan's Curve
• jordan11: Preparing the Internal Approximations of Simple Closed Curves
• jordan12: On the General Position of Special Polygons
• jordan13: Introducing Spans
• jordan14: Properties of the Internal Approximation of {J}ordan's Curve
• jordan15: Properties of the Upper and Lower Sequence on the Cage
• jordan16: On the Decomposition of a Simple Closed Curve into Two Arcs
• jordan17: The Ordering of Points on a Curve, Part {III}
• jordan18: The Ordering of Points on a Curve, Part {IV}
• jordan19: On the Upper and Lower Approximations of the Curve
• jordan1a: Gauges and Cages
• jordan1b: Some Properties of Cells and Arcs
• jordan1c: Some Properties of Cells and Gauges
• jordan1d: Gauges and Cages. { P } art { II }
• jordan1e: Upper and Lower Sequence of a Cage
• jordan1f: Some Remarks on Finite Sequences on Go-boards
• jordan1g: Upper and Lower Sequence on the Cage. Part II
• jordan1h: More on External Approximation of a Continuum
• jordan1i: Some Remarks on Clockwise Oriented Sequences on Go-boards
• jordan1j: Upper and Lower Sequence on the Cage, Upper and Lower Arcs
• jordan1k: On the Minimal Distance Between Set in {E}uclidean Space
• jordan20: Behaviour of an Arc Crossing a Line
• jordan21: On Some Points of a Simple Closed Curve
• jordan22: On Some Points of a Simple Closed Curve. {P}art {II}
• jordan23: Subsequences of Almost, Weakly and Poorly One-to-one Finite Sequences
• jordan24: Homeomorphisms of {J}ordan Curves
• jordan2b: Projections in n-Dimensional Euclidean Space to Each Coordinates
• jordan2c: Bounded Domains and Unbounded Domains
• jordan3: Reconstructions of Special Sequences
• jordan4: Subsequences of Standard Special Circular Sequences in $ { \cal E } ^2_ { \rm T } $
• jordan5a: Some Properties of Real Maps
• jordan5b: The Ordering of Points on a Curve, Part { I }
• jordan5c: The Ordering of Points on a Curve, Part { II }
• jordan5d: Bounding Boxes for Special Sequences in ${\calE}^2$
• jordan6: A Decomposition of Simple Closed Curves and an Order of Their Points
• jordan7: On a Dividing Function of the Simple Closed Curve into Segments
• jordan8: Gauges
• jordan9: Cages, external approximation of Jordan's curve
• jordan_a: On the Segmentation of a Simple Closed Curve
• knaster: Fix-points in complete lattices
• kolmog01: Kolmogorov's Zero-one Law
• kurato_0: On the {K}uratowski Limit Operators I
• kurato_1: On the {K}uratowski Closure-Complement Problem
• kurato_2: On the {K}uratowski Limit Operators
• l_hospit: The de l'Hospital Theorem
• lagra4sq: Lagrange's Four-Square Theorem
• lang1: Context-Free Grammar - Part 1
• laplace: Laplace Expansion
• latquasi: Formalization of Quasilattices
• latstone: Stone Lattices
• latsubgr: On the Lattice of Subgroups of a Group
• latsum_1: The Operation of Addition of Relational Structures
• lattad_1: Formalization of Generalized Almost Distributive Lattices
• lattba_1: Automatization of {T}ernary {B}oolean {A}lgebras
• lattice2: Finite Join and Finite Meet, and Dual Lattices
• lattice3: Complete Lattices
• lattice4: Homomorphisms of Lattices \\ Finite Join and Finite Meet
• lattice5: J\'onsson Theorem
• lattice6: Noetherian Lattices
• lattice7: Representation Theorem For Finite Distributive Lattices
• lattice8: J\'onsson Theorem about Representation of Modular Lattices
• latticea: Prime Filters and Ideals in Distributive Lattices
• lattices: Introduction to Lattice Theory
• latwal_1: On Weakly Associative Lattices and Near Lattices
• leibniz1: Leibniz's Series for Pi
• lexbfs: Recognizing Chordal Graphs: Lex BFS and MCS
• lfuzzy_0: Lattice of Fuzzy Sets
• lfuzzy_1: Transitive Closure of Fuzzy Relations
• limfunc1: The Limit of a Real Function at Infinity. Halflines. Real Sequence Divergent to Infinity
• limfunc2: One-Side Limits of a Real Function at a Point
• limfunc3: The Limit of a Real Function at a Point
• limfunc4: The Limit of a Composition of Real Functions
• liouvil1: Introduction to {L}iouville Numbers
• liouvil2: All Liouville Numbers are Transcendental
• lmod_6: Submodules
• lmod_7: Domains of Submodules, Join and Meet of Finite Sequences of Submodules and Quotient Modules
• lopban10: Multilinear Operator and Its Basic Properties
• lopban11: Continuity of Multilinear Operator on Normed Linear Spaces
• lopban12: Isomorphisms from the Space of Multilinear Operators
• lopban13: Invertible Operators on Banach Spaces
• lopban_1: Banach Space of Bounded Linear Operators
• lopban_2: The {B}anach Algebra of Bounded Linear Operators
• lopban_3: The Series on {B}anach Algebra
• lopban_4: The Exponential Function on {B}anach Algebra
• lopban_5: Uniform Boundedness Principle
• lopban_6: Open Mapping Theorem
• lopban_7: Banach's Continuous Inverse Theorem and Closed Graph Theorem
• lopban_8: Continuity of Bounded Linear Operators on Normed Linear Spaces
• lopban_9: Bilinear Operators on Normed Linear Spaces
• lopclset: Representation Theorem for Boolean Algebras
• lp_space: The Banach Space $l^p$
• lpspacc1: On $L^1$ Space Formed by Complex-valued Partial Functions
• lpspace1: On $L^1$ Space Formed by Real-valued Partial Functions
• lpspace2: On $L^p$ Space Formed by Real-valued Partial Functions
• ltlaxio1: The Axiomatization of Propositional Linear Time Temporal Logic
• ltlaxio2: The Derivations of Temporal Logic Formulas
• ltlaxio3: The Properties of Sets of Temporal Logic Subformulas
• ltlaxio4: Weak Completeness Theorem for Propositional Linear Time Temporal Logic
• ltlaxio5: Propositional Linear Time Temporal Logic with Initial Semantics
• lukasi_1: Propositional Calculus
• margrel1: Many-Argument Relations
• mathmorp: Preliminaries to Mathematical Morphology and Its Properties
• matrix10: Some Special Matrices of Real Elements and Their Properties
• matrix11: Basic Properties of Determinants of Square Matrices over a Field
• matrix12: Some Properties of Line and Column Operations on Matrices
• matrix13: Basic Properties of the Rank of Matrices over a Field
• matrix14: Invertibility of Matrices of Field Elements
• matrix15: Solutions of Linear Equations
• matrix16: Basic Properties of Circulant Matrices and Anti-circular Matrices
• matrix17: Some Basic Properties of Some Special Matrices, Part {III}
• matrix_0: Matrices.
• matrix_1: Abelian Group of Matrices
• matrix_3: The Product of Matrices of Elements of a Field and Determinants
• matrix_4: Calculation of Matrices of Field Elements. Part {I}
• matrix_5: A Theory of Matrices of Complex Elements
• matrix_6: Some Properties Of Some Special Matrices
• matrix_7: Determinant of Some Matrices of Field Elements
• matrix_8: Some Properties Of Some Special Matrices, Part {II}
• matrix_9: On the Permanent of a Matrix
• matrixc1: The Inner Product and Conjugate of Matrix of Complex Numbers
• matrixj1: Block Diagonal Matrices
• matrixj2: Jordan Matrix Decomposition
• matrixr1: A Theory of Matrices of Real Elements
• matrixr2: Determinant and Inverse of Matrices of Real Elements
• matrlin: Associated Matrix of Linear Map
• matrlin2: Linear Map of Matrices
• matroid0: Introduction to Matroids
• matrprob: The Definition of Finite Sequences and Matrices of Probability, and Addition of Matrices of Real Elements
• matrtop1: Linear Transformations of Euclidean Topological Spaces
• matrtop2: Linear Transformations of Euclidean Topological Spaces. Part {II}
• matrtop3: The Rotation Group
• mazurulm: Mazur-Ulam Theorem
• mboolean: Definitions and Basic Properties of Boolean & Union of Many Sorted Sets
• mcart_1: Tuples, Projections and Cartesian Products
• measur10: Product Pre-Measure
• measur11: Fubini's Theorem on Measure
• measur12: Reconstruction of the One-Dimensional Lebesgue Measure
• measure1: The $\sigma$-additive Measure Theory
• measure2: Several Properties of the $\sigma$-additive Measure
• measure3: Completeness of the $\sigma$-Additive Measure. Measure Theory
• measure4: Properties of Caratheodory's Measure
• measure5: Properties of the Intervals of Real Numbers
• measure6: Some Properties of the Intervals
• measure7: The One-Dimensional Lebesgue Measure As an Example of a Formalization in the Mizar Language of the Classical Definition of a Mathematical Object
• measure8: The Hopf Extension Theorem of Measure
• measure9: Construction of Measure from Semialgebra of Sets
• member_1: Collective Operations on Number-Membered Sets
• membered: On the Sets Inhabited by Numbers
• memstr_0: Memory Structures
• menelaus: Routh's, {M}enelaus' and Generalized {C}eva's Theorems
• mesfun10: Fatou's Lemma and the {L}ebesgue's Convergence Theorem
• mesfun11: Integral of Non Positive Functions
• mesfun12: Fubini's Theorem for Nonnegative or Nonpositive Functions
• mesfun13: Fubini's Theorem
• mesfun14: Relationship between the {R}iemann and {L}ebesgue Integrals
• mesfun6c: Integral of Complex-Valued Measurable Function
• mesfun7c: The Measurability of Complex-Valued Functional Sequences
• mesfun9c: Lebesgue's Convergence Theorem of Complex-Valued Function
• mesfunc1: Definitions and Basic Properties of Measurable Functions
• mesfunc2: Measurability of Extended Real Valued Functions
• mesfunc3: Lebesgue Integral of Simple Valued Function
• mesfunc4: Linearity of {L}ebesgue Integral of Simple Valued Function
• mesfunc5: Integral of Measurable Function
• mesfunc6: Integral of Real-valued Measurable Function
• mesfunc7: The First Mean Value Theorem for Integrals
• mesfunc8: Egoroff's Theorem
• mesfunc9: The Lebesgue Monotone Convergence Theorem
• metric_1: Metric Spaces
• metric_2: On Pseudometric Spaces
• metric_3: Metrics in Cartesian Product
• metric_6: Sequences in Metric Spaces
• metrizts: Basic Properties of Metrizable Topological Spaces
• mfold_0: Topological Manifolds
• mfold_1: The Definition of Topological Manifolds
• mfold_2: Planes and Spheres as Topological Manifolds. Stereographic Projection
• midsp_1: Midpoint algebras
• midsp_2: Atlas of Midpoint Algebra
• midsp_3: Reper Algebras
• mmlquer2: The Semantics of MML Query -- Ordering
• mmlquery: Semantic of MML Query
• mod_2: Rings and Modules - Part II
• mod_3: Free Modules
• mod_4: Opposite Rings, Modules and their Morphisms
• modal_1: Introduction to Modal Propositional Logic
• modcat_1: Category of Left Modules
• modelc_1: Model Checking, Part {I}
• modelc_2: Model Checking, Part II
• modelc_3: Model Checking, Part {III}
• moebius1: On the Properties of the {M}\"obius Function
• moebius2: On Square-free Numbers
• moebius3: Sequences of Prime Reciprocals -- Preliminaries
• monoid_0: Monoids
• monoid_1: Monoid of Multisets and Subsets
• morph_01: Morphology for Image Processing, Part {I}
• msafree: Free Many Sorted Universal Algebra
• msafree1: A Scheme for Extensions of Homomorphisms of Manysorted Algebras
• msafree2: Preliminaries to Circuits, II
• msafree3: Yet another construction of free algebra
• msafree4: Free Term Algebras
• msafree5: Term Context
• msalimit: Inverse Limits of Many Sorted Algebras
• msaterm: Terms over many sorted universal algebra
• msinst_1: Examples of Category Structures
• msscyc_1: The Correspondence Between Monotonic Many Sorted Signatures and Well-Founded Graphs. {P}art {I}
• msscyc_2: The Correspondence Between Monotonic Many Sorted Signatures and Well-Founded Graphs. {P}art {II}
• mssubfam: Certain Facts about Families of Subsets of Many Sorted Sets
• mssublat: The Correspondence Between Lattices of Subalgebras of Universal Algebras and Many Sorted Algebras
• msualg_1: Many Sorted Algebras
• msualg_2: Subalgebras of a Many Sorted Algebra. Lattice of Subalgebras
• msualg_3: Homomorphisms of Many Sorted Algebras
• msualg_4: Many Sorted Quotient Algebra
• msualg_5: Lattice of Congruences in a Many Sorted Algebra
• msualg_6: Translations, Endomorphisms, and Stable Equational Theories
• msualg_7: More on the Lattice of Many Sorted Equivalence Relations
• msualg_8: More on the Lattice of Congruences in a Many Sorted Algebra
• msualg_9: On the Trivial Many Sorted Algebras and Many Sorted Congruences
• msuhom_1: The Correspondence Between Homomorphisms of Universal Algebra & Many Sorted Algebra
• multop_1: Three-Argument Operations and Four-Argument Operations
• music_s1: {P}ythagorean Tuning: Pentatonic and Heptatonic Scale
• mycielsk: The {M}ycielskian of a Graph
• nagata_1: The {N}agata-Smirnov Theorem. {P}art {I}
• nagata_2: The {N}agata-Smirnov Theorem. {P}art {II}
• nat_1: The Fundamental Properties of Natural Numbers
• nat_2: Natural Numbers
• nat_3: Fundamental {T}heorem of {A}rithmetic
• nat_4: Pocklington's Theorem and {B}ertrand's Postulate
• nat_5: The Perfect Number Theorem and Wilson's Theorem
• nat_6: Proth Numbers
• nat_d: Divisibility of Natural Numbers
• nat_lat: The Lattice of Natural Numbers and The Sublattice of it. The Set of Prime Numbers
• nattra_1: Natural Transformations. Discrete Categories
• nbvectsp: $n$-dimensional Binary Vector Spaces
• ncfcont1: Continuous Functions on Real and Complex Normed Linear Spaces
• ncfcont2: Uniform Continuity of Functions on Normed Complex Linear Spaces
• ndiff10: Inverse Function Theorem -- Part {I}
• ndiff_1: The Differentiable Functions on Normed Linear Spaces
• ndiff_2: Differentiable Functions on Normed Linear Spaces. {P}art {II}
• ndiff_3: Differentiable Functions into Real Normed Spaces
• ndiff_4: The Differentiable Functions from $\mathbbR$ into ${\mathbbR}^n$
• ndiff_5: Differentiable Functions on Normed Linear Spaces
• ndiff_6: Differentiation in Normed Spaces
• ndiff_7: Isometric Differentiable Functions on Real Normed Space
• ndiff_8: Implicit Function Theorem -- Part {I}
• ndiff_9: Implicit Function Theorem -- Part {II}
• neckla_2: The Class of Series-Parallel Graphs, {II}
• neckla_3: The Class of Series-Parallel Graphs, {III}
• necklace: The Class of Series-Parallel Graphs, {I}
• nelson_1: Two Axiomatizations of {N}elson Algebras
• net_1: Some Elementary Notions of the Theory of Petri Nets
• newton: Factorial and Newton coefficients
• newton01: Some Remarkable Identities Involving Numbers
• newton02: Fermat's Little Theorem via Divisibility of {N}ewton's Binomial
• newton03: Prime Factorization of Sums and Differences of Two Like Powers
• newton04: On Subnomials
• newton05: Parity as a Property of Integers
• nfcont_1: The Continuous Functions on Normed Linear Spaces
• nfcont_2: The Uniform Continuity of Functions on Normed Linear Spaces
• nfcont_3: More on Continuous Functions on Normed Linear Spaces
• nfcont_4: More on the Continuity of Real Functions
• niven: Niven's Theorem
• nomin_1: Simple-named complex-valued nominative data -- definition and basic operations
• nomin_2: On an algorithmic algebra over simple-named complex-valued nominative data
• nomin_3: An inference system of an extension of Floyd-Hoare logic for partial predicates
• nomin_4: Partial correctness of GCD algorithm
• nomin_5: Partial Correctness of a Factorial Algorithm
• nomin_6: Partial Correctness of a Power Algorithm
• nomin_7: Partial Correctness of a Fibonacci Algorithm
• nomin_8: General theory and tools for proving algorithms in nominative data systems
• nomin_9: Partial correctness of an algorithm computing Lucas sequences
• normform: Algebra of Normal Forms
• normsp_0: Preliminaries to Normed Spaces
• normsp_1: Real Normed Space
• normsp_2: Baire's Category Theorem and Some Spaces Generated from Real Normed Space
• normsp_3: Topological Properties of Real Normed Space
• normsp_4: Separability of Real Normed Spaces and Its Basic Properties
• ntalgo_1: Extended Euclidean Algorithm and CRT Algorithm
• ntalgo_2: Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm
• number01: Elementary Number Theory Problems. {P}art {I}
• number02: Elementary Number Theory Problems. {P}art {II}
• numbers: Subsets of Complex Numbers
• numeral1: On the Representation of Natural Numbers in Positional Numeral Systems
• numeral2: More on Divisibility Criteria for Selected Primes
• numerals: Numerals - Requirements
• numpoly1: Polygonal Numbers
• o_ring_1: Ordered Rings - Part I
• openlatt: Representation Theorem for Heyting Lattices
• oposet_1: Basic Notions and Properties of Orthoposets
• oppcat_1: Opposite Categories and Contravariant Functors
• ordeq_01: Contracting Mapping on Normed Linear Space
• ordeq_02: Differential Equations on Functions from $\mathbbR$ into Real {B}anach Space
• orders_1: Partially Ordered Sets
• orders_2: Kuratowski - Zorn Lemma
• orders_3: On the Category of Posets
• orders_4: On the Isomorphism Between Finite Chains
• orders_5: About Quotient Orders and Ordering Sequences
• ordinal1: The Ordinal Numbers. Transfinite Induction and Defining by Transfinite Induction
• ordinal2: Sequences of Ordinal Numbers. Beginnings of Ordinal Arithmetics
• ordinal3: Ordinal Arithmetics
• ordinal4: Increasing and Continuous Ordinal Sequences
• ordinal5: Epsilon Numbers and Cantor Normal Form
• ordinal6: Veblen Hierarchy
• ordinal7: Natural Addition of Ordinals
• ortsp_1: Construction of a bilinear symmetric form in orthogonal vector space
• osafree: Free Order Sorted Universal Algebra
• osalg_1: Order Sorted Algebras
• osalg_2: Subalgebras of a Order Sorted Algebra. {L}attice of Subalgebras
• osalg_3: Homomorphisms of Order Sorted Algebras
• osalg_4: Order Sorted Quotient Algebra
• papdesaf: Fanoian, Pappian and Desarguesian Affine Spaces
• pappus: Pappus's Hexagon Theorem in Real Projective Plane
• pardepap: Elementary Variants of Affine Configurational Theorems
• parsp_1: Parallelity Spaces
• parsp_2: Fano-Desargues Parallelity Spaces
• partfun1: Partial Functions
• partfun2: Partial Functions from a Domain to a Domain
• partfun3: On the Real Valued Functions
• partfun4: On the Real Valued Functions
• partit1: A theory of partitions, { I }
• partit_2: Classes of Independent Partitions
• partpr_1: Kleene Algebra of Partial Predicates
• partpr_2: On algebras of algorithms and specifications over uninterpreted data
• pascal: Pascal's Theorem in Real Projective Plane
• pasch: Classical and Non--classical Pasch Configurations in Ordered Affine Planes
• pboole: Manysorted Sets
• pcomps_1: Paracompact and Metrizable Spaces
• pcomps_2: On Paracompactness of Metrizable Spaces
• pcs_0: Basic Operations on Preordered Coherent Spaces
• pdiff_1: Partial Differentiation on Normed Linear Spaces $ {\cal R}^n$
• pdiff_2: Partial Differentiation of Real Binary Functions
• pdiff_3: Second-order Partial Differentiation of Real Binary Functions
• pdiff_4: Partial Differentiation of Real Ternary Functions
• pdiff_5: Second-order Partial Differentiation of Real Ternary Functions
• pdiff_6: Differentiation of Vector-Valued Functions on $n$-Dimensional Real Normed Linear Spaces
• pdiff_7: Partial Differentiation of Vector-Valued Functions on $n$-Dimensional Real Normed Linear Spaces
• pdiff_8: Partial Differentiation, Differentiation and Continuity on $n$-Dimensional Real Normed Linear Spaces
• pdiff_9: Higher Order Partial Differentiation
• pdiffeq1: A Simple Example for Linear Partial Differential Equations and Its Solution Using the Method of Separation of Variables
• pells_eq: The Pell's Equation
• pencil_1: On Segre's Product of Partial Line Spaces
• pencil_2: On Cosets in Segre's Product of Partial Linear Spaces
• pencil_3: On the Characterization of Collineations of the Segre Product of Strongly Connected Partial Linear Spaces
• pencil_4: Spaces of Pencils, {G}rassmann Spaces, and Generalized {V}eronese Spaces
• pepin: Public-Key Cryptography and Pepin's Test for the Primality of Fermat Numbers
• peterson: Event-based Proof of the Mutual Exclusion Property of {P}eterson's Algorithm
• petri: Basic Petri Net Concepts. Place/Transition Net Structure, Deadlocks, Traps, Dual Nets
• petri_2: Cell Petri Net Concepts
• petri_3: Formulation of Cell Petri Nets
• petri_df: The Formalization of Decision Free {P}etri Net
• pl_axiom: The Axiomatization of Propositional Logic
• pnproc_1: Processes in {P}etri nets
• polnot_1: Polish Notation
• polyalg1: The Algebra of Polynomials
• polydiff: Differentiability of Polynomials over Reals
• polyeq_1: Solving Roots of Polynomial Equations of Degree 2 and 3 with Real Coefficients
• polyeq_2: Solving Roots of Polynomial Equation of Degree 4 with Real Coefficients
• polyeq_3: Solving Complex Roots of Polynomial Equation of Degree 2 and 3 with Complex Coefficients
• polyeq_4: Solving the Roots of the Special Polynomial Equation with Real Coefficients
• polyeq_5: Solution of Cubic and Quartic Equations
• polyform: Euler's Polyhedron Formula
• polynom1: Multivariate polynomials with arbitrary number of variables
• polynom2: Evaluation of Multivariate Polynomials
• polynom3: The Ring of Polynomials
• polynom4: Evaluation of Polynomials
• polynom5: Fundamental Theorem of Algebra
• polynom6: On polynomials with coefficients in a ring of polynomials
• polynom7: More About Polynomials: Monomials and Constant Polynomials
• polynom8: Multiplication of Polynomials using {D}iscrete {F}ourier {T}ransformation
• polyred: Polynomial Reduction
• polyvie1: Vieta's Formula about the Sum of Roots of Polynomials
• poset_1: Fix-point Theorem for Continuous Functions on Chain-complete Posets
• poset_2: Definition of Flat Poset and Existence Theorems for Recursive Call
• power: Real Exponents and Logarithms
• pralg_1: Product of Family of Universal Algebras
• pralg_2: Products of Many Sorted Algebras
• pralg_3: More on Products of Many Sorted Algebras
• pre_circ: Preliminaries to Circuits, I
• pre_ff: Two Programs for {\bf SCM}. Part I - Preliminaries
• pre_poly: Preliminaries to Polynomials
• pre_topc: Topological Spaces and Continuous Functions
• prefer_1: Introduction to Formal Preference Spaces
• prelamb: Preliminaries to the Lambek Calculus
• prepower: Integer and Rational Exponents
• prgcor_1: Correctness of Non Overwriting Programs. {P}art {I}
• prgcor_2: Logical Correctness of Vector Calculation Programs
• prob_1: $\sigma$-Fields and Probability
• prob_2: Probability. Independence of Events and Conditional Probability
• prob_3: Set Sequences and Monotone Class
• prob_4: The Relevance of Measure and Probability and Definition of Completeness of Probability
• procal_1: Calculus of Propositions
• projdes1: Desargues Theorem In Projective 3-Space
• projpl_1: Projective {P}lanes
• projred1: Incidence Projective Space (a reduction theorem in a plane)
• projred2: On Projections in Projective Planes. Part II
• prsubset: Dynamic Programming for the Subset Sum Problem
• prvect_1: Product of Families of Groups and Vector Spaces
• prvect_2: The Product Space of Real Normed Spaces and Its Properties
• prvect_3: Cartesian Products of Family of Real Linear Spaces
• prvect_4: The 3-fold Product Space of Real Normed Spaces and its Properties
• pscomp_1: Bounding boxes for compact sets in ${\calE}^2$
• pua2mss1: Minimal Manysorted Signature for Partial Algebra
• pythtrip: Pythagorean triples
• pzfmisc1: Some Basic Properties of Many Sorted Sets
• qc_lang1: A First Order Language
• qc_lang2: Connectives and Subformulae of the First Order Language
• qc_lang3: Variables in Formulae of the First Order Language
• qc_lang4: The Subformula Tree of a Formula of the First Order Language
• qc_trans: Transition of Consistency and Satisfiability under Language Extensions
• qmax_1: The Fundamental Logic Structure in Quantum Mechanics
• quantal1: Quantales
• quatern2: Inner Products, Group, Ring of Quaternion Numbers
• quatern3: Some Operations on Quaternion Numbers
• quaterni: The Quaternion Numbers
• quin_1: Quadratic Inequalities
• quofield: The Field of Quotients over an Integral Domain
• radix_1: Definitions of Radix-2k Signed-Digit number and its adder algorithm
• radix_2: High-speed algorithms for RSA cryptograms
• radix_3: Improvement of Radix-$2^k$ Signed-Digit Number for High Speed Circuit
• radix_4: High Speed Adder Algorithm with Radix-$2^k$ SD_Sub Number
• radix_5: Magnitude Relation Properties of Radix-$2^k$ SD Number
• radix_6: High Speed Modulo Calculation Algorithm with Radix-$2^k$ SD Number
• ramsey_1: Ramsey's Theorem
• random_1: Probability on Finite Set and Real Valued Random Variables
• random_2: Probability Measure on Discrete Spaces and Algebra of Real Valued Random Variables
• random_3: Random Variables and Product of Probability Spaces
• ranknull: The Rank+Nullity Theorem
• rat_1: Basic Properties of Rational Numbers
• ratfunc1: Introduction to Rational Functions
• rcomp_1: Topological Properties of Subsets in Real Numbers
• rcomp_3: Properties of Connected Subsets of the Real Line
• real: Basic Properties of Real Numbers - Requirements
• real_1: Basic Properties of Real Numbers
• real_3: Simple Continued Fractions and Their Convergents
• real_lat: The Lattice of Real Numbers. The Lattice of Real Functions
• real_ns1: Completeness of the Real {E}uclidean Space
• real_ns2: Real Vector Space and Related Notions
• real_ns3: Finite Dimensional Real Normed Spaces are Proper Metric Spaces
• realalg1: Ordered Rings and Fields
• realalg2: Formally Real Fields
• realset1: Group and Field Definitions
• realset2: Properties of Fields
• realset3: Several Properties of Fields. Field Theory
• rearran1: Introduction to Theory of Rearrangment
• recdef_1: Recursive Definitions
• recdef_2: Recursive Definitions. {P}art {II}
• relat_1: Relations and Their Basic Properties
• relat_2: Properties of Binary Relations
• reloc: Relocatability
• relset_1: Relations Defined on Sets
• relset_2: Properties of First and Second Order Cutting of Binary Relations
• revrot_1: Rotating and reversing.(Finite sequences)
• rewrite1: Reduction Relations
• rewrite2: String Rewriting Systems
• rewrite3: Labelled State Transition Systems
• rfinseq: Functions and Finite Sequences of Real Numbers
• rfinseq2: Sorting Operators for Finite Sequences
• rfunct_1: Partial Functions from a Domain to the Set of Real Numbers
• rfunct_2: Properties of Real Functions
• rfunct_3: Properties of Partial Functions from a Domain to the Set of Real Numbers
• rfunct_4: Introduction to Several Concepts of Convexity and Semicontinuity for Function from REAL to REAL
• rinfsup1: Inferior Limit and Superior Limit of Sequences of Real Numbers
• rinfsup2: Inferior Limit, Superior Limit and Convergence of Sequences of Extended Real Numbers
• ring_1: Quotient Rings
• ring_2: The First Isomorphism Theorem and Other Properties of Rings
• ring_3: Characteristic of Rings; Prime Fields
• ring_4: Some Algebraic Properties of Polynomial Rings
• ring_5: On Roots of Polynomials and Algebraically Closed Fields
• ringcat1: Category of Rings
• ringder1: Derivation of Commutative Rings \& {L}eibnitz Formula for Power of Derivation
• ringfrac: {R}ings of {F}ractions and {L}ocalization
• rlaffin1: Affine Independence in Vector Spaces
• rlaffin2: The Geometric Interior in Real Linear Spaces
• rlaffin3: Continuity of Barycentric Coordinates in Euclidean Topological Spaces
• rlsub_1: Subspaces and Cosets of Subspaces in Real Linear Space
• rlsub_2: Operations on Subspaces in Real Linear Space
• rltopsp1: Introduction to Real Linear Topological Spaces
• rlvect_1: Vectors in Real Linear Space
• rlvect_2: Linear Combinations in Real Linear Space
• rlvect_3: Basis of Real Linear Space
• rlvect_4: Subspaces of Real Linear Space Generated by One, Two, or Three Vectors and Their Cosets
• rlvect_5: The Steinitz Theorem and the Dimension of a Real Linear Space
• rlvect_x: Formalization of Integral Linear Space
• rmod_2: Submodules and Cosets of Submodules in Right Module over Associative Ring
• rmod_3: Operations on Submodules in Right Module over Associative Ring
• rmod_4: Linear Combinations in Right Module over Associative Ring
• robbins1: Robbins Algebras vs. Boolean Algebras
• robbins2: On the Two Short Axiomatizations of Ortholattices
• robbins3: Formalization of Ortholattices via Orthoposets
• robbins4: Orthomodular Lattices
• robbins5: On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander
• rolle: Average Value Theorems for Real Functions of One Variable
• roughif1: Formal Development of Rough Inclusion Functions
• roughif2: Developing Complementary Rough Inclusion Functions
• roughs_1: Basic Properties of Rough Sets and Rough Membership Function
• roughs_2: Relational Formal Characterization of Rough Sets
• roughs_3: Binary Relations-Based Rough Sets -- An Automated Approach
• roughs_4: Topological Interpretation of Rough Sets
• roughs_5: Formalizing Two Generalized Approximation Operators
• rpr_1: Introduction to Probability
• rsspace: Real Linear Space of Real Sequences
• rsspace2: Hilbert Space of Real Sequences
• rsspace3: Banach Space of Absolute Summable Real Sequences
• rsspace4: Banach Space of Bounded Real Sequences
• rusub_1: Subspaces and Cosets of Subspace of Real Unitary Space
• rusub_2: Operations on Subspaces in Real Unitary Space
• rusub_3: Linear Combinations in Real Unitary Space
• rusub_4: Dimension of Real Unitary Space
• rusub_5: Topology of Real Unitary Space
• rvsum_1: The Sum and Product of Finite Sequences of Real Numbers
• rvsum_2: The Sum and Product of Finite Sequences of Complex Numbers
• rvsum_3: Cauchy Mean Theorem
• rvsum_4: Concatenation of Finite Sequences
• scheme1: Schemes of Existence of some Types of Functions
• schems_1: Schemes
• scm_1: Development of Terminology for {\bf SCM}
• scm_comp: A compiler of arithmetic expressions for { \bf SCM }
• scm_halt: Initialization Halting Concepts and Their Basic Properties of SCM+FSA
• scm_inst: On a Mathematical Model of Programs
• scmbsort: Bubble Sort on SCM+FSA
• scmfsa10: On the Instructions of { \bf SCM+FSA }
• scmfsa6a: On the compositions of macro instructions
• scmfsa6b: On the compositions of macro instructions, Part II
• scmfsa6c: On the compositions of macro instructions, Part III
• scmfsa7b: Constant assignment macro instructions of SCM+FSA, Part II
• scmfsa8a: Conditional branch macro instructions of SCM+FSA, Part I (preliminary)
• scmfsa8b: Conditional branch macro instructions of SCM+FSA, Part II
• scmfsa8c: The {\bf loop} and {\bf Times} Macroinstruction for {\SCMFSA}
• scmfsa9a: The { \bf while } macro instructions of SCM+FSA, Part { II }
• scmfsa_1: An Extension of { \bf SCM }
• scmfsa_2: The { \bf SCM_FSA } computer
• scmfsa_3: Computation in { \bf SCM_FSA }
• scmfsa_4: Modifying addresses of instructions of { \bf SCM_FSA }
• scmfsa_5: Relocability for { \bf SCM_FSA }
• scmfsa_7: Some Multi-instructions defined by sequence of instructions of SCM+FSA
• scmfsa_9: While Macro Instructions of SCM+FSA
• scmfsa_i: The Instructions for SCM+FSA Computer
• scmfsa_m: On the memory of SCM+FSA
• scmfsa_x: On SCM+FSA Programs
• scmisort: Insert Sort on SCM+FSA
• scmp_gcd: Recursive Euclid's Algorithm
• scmpds_1: A Small Computer Model with Push-Down Stack
• scmpds_2: The SCMPDS Computer and the Basic Semantics of Its Instructions
• scmpds_3: Computation and Program Shift in the SCMPDS Computer
• scmpds_4: The Construction and shiftability of Program Blocks for SCMPDS
• scmpds_5: Computation of Two Consecutive Program Blocks for SCMPDS
• scmpds_6: The Construction and Computation of Conditional Statements for SCMPDS
• scmpds_7: The Construction and Computation of For-loop Programs for SCMPDS
• scmpds_8: The Construction and Computation of While-loop Programs for SCMPDS
• scmpds_9: SCMPDS Is Not Standard
• scmpds_i: The Instructions for the SCMPDS computer
• scmring1: The Construction of { \bf SCM } over Ring
• scmring2: The Basic Properties of { \bf SCM } over Ring
• scmring3: The Properties of Instructions of { \bf SCM } over Ring
• scmring4: Relocability for { \bf SCM } over Ring
• scmringi: The Construction of { \bf SCM } over Ring
• scmyciel: Simple Graphs as Simplicial Complexes: the {M}ycielskian of a Graph
• scpinvar: Justifying the Correctness of Fibonacci Sequence and Euclid's Algorithm by Loop Invariant
• scpisort: Insert Sort on SCMPDS
• scpqsort: Quick Sort on SCMPDS
• semi_af1: Semi-Affine Space
• seq_1: Real Sequences and Basic Operations on Them
• seq_2: Convergent Sequences and the Limit of Sequences
• seq_4: Convergent Real Sequences. Upper and Lower Bound of Sets of Real Numbers
• seqfunc: Functional Sequence from a Domain to a Domain
• seqfunc2: Functional Sequence in Norm Space
• seqm_3: Monotone Real Sequences. Subsequences
• series_1: Series
• series_2: Partial Sum of Some Series
• series_3: On the Partial Product of Series and Related Basic Inequalities
• series_4: Partial Sum and Partial Product of Some Series
• series_5: On the Partial Product and Partial Sum of Series and Related Basic Inequalities
• setfam_1: Families of Sets
• setlim_1: Limit of Sequence of Subsets
• setlim_2: Some Equations Related to the Limit of Sequence of Subsets
• setwiseo: Semilattice Operations on Finite Subsets
• setwop_2: Semigroup operations on finite subsets
• sf_mastr: Memory handling for SCM+FSA
• sfmastr1: On the Composition of non-parahalting Macro Instructions
• sfmastr2: Another { \bf times } Macro Instruction
• sfmastr3: The { \bf for } (going up) Macro Instruction
• sgraph1: The Formalisation of Simple Graphs
• sheffer1: Axiomatization of {B}oolean Algebras Based on Sheffer Stroke
• sheffer2: Short {S}heffer Stroke-Based Single Axiom for {B}oolean Algebras
• simplex0: Abstract Simplicial Complexes
• simplex1: Sperner's Lemma
• simplex2: Brouwer Fixed Point Theorem for Simplexes
• sin_cos: Trigonometric Functions and Existence of Circle Ratio
• sin_cos2: Properties of Trigonometric Function
• sin_cos3: Trigonometric Functions on Complex Space
• sin_cos4: Formulas And Identities of Trigonometric Functions
• sin_cos5: Formulas And Identities of Trigonometric Functions
• sin_cos6: Inverse Trigonometric Functions Arcsin and Arccos
• sin_cos7: Formulas And Identities of Inverse Hyperbolic Functions
• sin_cos8: Formulas and Identities of Hyperbolic Functions
• sin_cos9: Inverse Trigonometric Functions Arctan and Arccot
• sincos10: Inverse Trigonometric Functions Arcsec1, Arcsec2, Arccosec1 and Arccosec2
• sppol_1: Extremal Properties of Vertices on Special Polygons I
• sppol_2: Special Polygons
• sprect_1: On Rectangular Finite Sequences of the Points of the Plane
• sprect_2: On the Order on a Special Polygon
• sprect_3: Some properties of special polygonal curves
• sprect_4: On the components of the complement of a special polygonal curve
• sprect_5: Again on the Order on a Special Polygon
• square_1: Some Properties of Real Numbers. Operations: min, max, square, and square root
• srings_1: Semiring of Sets
• srings_2: Semiring of Sets: Examples
• srings_3: $\sigma$-ring and $\sigma$-algebra of Sets
• srings_4: Finite Product of Semiring of Sets
• srings_5: Chebyshev Distance
• stacks_1: Representation Theorem for Stacks
• stirl2_1: Stirling Numbers of the Second Kind
• struct_0: Preliminaries to Structures
• sublemma: Coincidence Lemma and Substitution Lemma
• subset: Basic Properties of Subsets - Requirements
• subset_1: Properties of Subsets
• substlat: Lattice of Substitutions
• substut1: Substitution in First-Order Formulas: Elementary Properties
• substut2: Substitution in First-Order Formulas -- Part II. {T}he Construction of First-Order Formulas
• supinf_1: Infimum and Supremum of the Set of Real Numbers. Measure Theory
• supinf_2: Series of Positive Real Numbers. Measure Theory
• symsp_1: Construction of a bilinear antisymmetric form in symplectic vector space
• sysrel: Some Properties of Binary Relations
• t_0topsp: $T_0$ Topological Spaces
• t_1topsp: On $T_{1}$ Reflex of Topological Space
• tarski: Tarski {G}rothendieck Set Theory
• tarski_0: Axioms of Tarski {G}rothendieck Set Theory
• tarski_a: Tarski {G}rothendieck Set Theory -- Tarski's Axiom A
• taxonom1: Lower Tolerance. {P}reliminaries to {W}roclaw Taxonomy
• taxonom2: Hierarchies and Classifications of Sets
• taylor_1: The {T}aylor Expansions
• taylor_2: The {M}aclaurin Expansions
• tbsp_1: Totally Bounded Metric Spaces
• tdgroup: A Construction of an Abstract Space of Congruence of Vectors
• tdlat_1: The Lattice of Domains of a Topological Space
• tdlat_2: Completeness of the Lattices of Domains of a Topological Space
• tdlat_3: The Lattice of Domains of an Extremally Disconnected Space
• termord: Term Orders
• tex_1: On Discrete and Almost Discrete Topological Spaces
• tex_2: Maximal Discrete Subspaces of Almost Discrete Topological Spaces
• tex_3: On Nowhere and Everywhere Dense Subspaces of Topological Spaces
• tex_4: Maximal Anti-Discrete Subspaces of Topological Spaces
• tietze: Tietze {E}xtension {T}heorem
• tietze_2: Tietze Extension Theorem for $n$-dimensional Spaces
• tmap_1: Continuity of Mappings over the Union of Subspaces
• toler_1: Relations of Tolerance
• topalg_1: The Fundamental Group
• topalg_2: The Fundamental Group of Convex Subspaces of TOP-REAL n
• topalg_3: On the Isomorphism of Fundamental Groups
• topalg_4: On the Fundamental Groups of Products of Topological Spaces
• topalg_5: The Fundamental Group of the Circle
• topalg_6: Fundamental Group of $n$-sphere for $n \geq 2$
• topalg_7: Commutativeness of Fundamental Groups of Topological Groups
• topdim_1: Small {I}nductive {D}imension of {T}opological {S}paces
• topdim_2: Small Inductive Dimension of Topological Spaces, Part {II}
• topgen_1: On the Boundary and Derivative of a Set
• topgen_2: On the characteristic and weight of a topological space
• topgen_3: On constructing topological spaces and Sorgenfrey line
• topgen_4: On the {B}orel Families of Subsets of Topological Spaces
• topgen_5: Niemytzki Plane -- an Example of {T}ychonoff Space Which Is Not $T_4$
• topgen_6: Some Properties of the {S}orgenfrey Line and the {S}orgenfrey Plane
• topgrp_1: The Definition and Basic Properties of Topological Groups
• topmetr: Metric Spaces as Topological Spaces - Fundamental Concepts
• topmetr2: Some Facts about Union of Two Functions and Continuity of Union of Functions
• topmetr3: Sequences of Metric Spaces and an Abstract Intermediate Value Theorem
• topmetr4: Compactness in Metric Spaces
• topreal1: The Topological Space ${\calE}^2_{\rm T}$. Arcs, Line Segments and Special Polygonal Arcs
• topreal2: The Topological Space ${\calE}^2_{\rm T}$. Simple Closed Curves
• topreal3: Basic Properties of Connecting Points with Line Segments in ${\calE}^2_{\rm T}$
• topreal4: Connectedness Conditions Using Polygonal Arcs
• topreal5: Intermediate Value Theorem and Thickness of Simple Closed Curves
• topreal6: Compactness of the Bounded Closed Subsets of TOP-REAL 2
• topreal7: Homeomorphism between [:TOP-REAL i,TOP-REAL j:] and TOP-REAL (i+j)
• topreal8: More on the Finite Sequences on the Plane
• topreal9: Intersections of Intervals and Balls in TOP-REAL n
• topreala: Some Properties of Rectangles on the Plane
• toprealb: Some Properties of Circles on the Plane
• toprealc: On the Continuity of Some Functions
• toprns_1: Sequences in $R^n$
• tops_1: Subsets of Topological Spaces
• tops_2: Families of Subsets, Subspaces and Mappings in Topological Spaces
• tops_3: Remarks on Special Subsets of Topological Spaces
• tops_4: Miscellaneous Facts about Open Functions and Continuous Functions
• tops_5: Some Remarks about Product Spaces
• topzari1: {Z}ariski {T}opology
• transgeo: Transformations in Affine Spaces
• translac: Translations in Affine Planes
• treal_1: The Brouwer Fixed Point Theorem for Intervals
• trees_1: Introduction to Trees
• trees_2: K\"onig's Lemma
• trees_3: Sets and Functions of Trees and Joining Operations of Trees
• trees_4: Joining of Decorated Trees
• trees_9: Subtrees
• trees_a: Replacement of Subtrees in a Tree
• triang_1: On the concept of the triangulation
• tsep_1: Separated and Weakly Separated Subspaces of Topological Spaces
• tsep_2: On a Duality Between Weakly Separated Subspaces of Topological Spaces
• tsp_1: On Kolmogorov Topological Spaces
• tsp_2: Maximal Kolmogorov Subspaces of a Topological Space as Stone Retracts of the Ambient Space
• turing_1: Introduction to Turing Machines
• twoscomp: 2's Complement Circuit. Part I. Boolean Operators and 2's Complement Circuit Properties
• unialg_1: Basic Notation of Universal Algebra
• unialg_2: Subalgebras of the Universal Algebra. Lattices of Subalgebras
• unialg_3: On the Lattice of Subalgebras of a Universal Algebra
• uniform1: Lebesgue's Covering Lemma, Uniform Continuity and Segmentation of Arcs
• uniform2: Quasi-uniform Space
• uniform3: Uniform Space
• uniroots: Primitive Roots of Unity and Cyclotomic Polynomials
• uproots: Little {B}ezout Theorem (Factor Theorem)
• urysohn1: Dyadic Numbers and $T_4$ Topological Spaces
• urysohn2: Some Properties of Dyadic Numbers and Intervals
• urysohn3: Urysohn Lemma
• valuat_1: Interpretation and Satisfiability in the First Order Logic
• valued_0: Number-Valued Functions
• valued_1: Properties of Number-Valued Functions
• valued_2: Arithmetic Operations on Functions from Sets into Functional Sets
• vectmetr: Real Linear-Metric Space and Isometric Functions
• vectsp10: Quotient Vector Spaces and Functionals
• vectsp11: Eigenvalues of a Linear Transformation
• vectsp12: Isomorphism Theorem on Vector Spaces over a Ring
• vectsp_1: Abelian Groups, Fields and Vector Spaces
• vectsp_2: Construction of Rings and Left-, Right-, and Bi-Modules over a Ring
• vectsp_4: Subspaces and Cosets of Subspaces in Vector Space
• vectsp_5: Operations on Subspaces in Vector Space
• vectsp_6: Linear Combinations in Vector Space
• vectsp_7: Basis of Vector Space
• vectsp_8: On the Lattice of Subspaces of Vector Space
• vectsp_9: Steinitz Theorem and Dimension of a Vector Space
• vfunct_1: Algebra of Vector Functions
• vfunct_2: Algebra of Complex Vector Valued Functions
• vsdiff_1: Difference of Function on Vector Space over $\mathbbF$
• wallace1: Stability of the 7-3 Compressor Circuit for {W}allace Tree. Part {I}
• waybel10: Closure Operators and Subalgebras
• waybel11: Scott Topology
• waybel12: On the Baire Category Theorem
• waybel13: Algebraic and Arithmetic Lattices
• waybel14: The Scott Topology, Part II
• waybel15: More on the Algebraic and Arithmetic Lattices
• waybel16: Completely-Irreducible Elements
• waybel17: Scott-Continuous Functions
• waybel18: Injective Spaces
• waybel19: The Lawson Topology
• waybel20: Kernel Projections and Quotient Lattices
• waybel21: Lawson Topology in Continuous Lattices
• waybel22: Representation theorem for free continuous lattices
• waybel23: Bases of Continuous Lattices
• waybel24: Scott-Continuous Functions, Part II
• waybel25: Injective Spaces, Part { II }
• waybel26: Continuous Lattices between T$_0$ Spaces
• waybel27: Function Spaces in the Category of Directed Suprema Preserving Maps
• waybel28: Lim-inf Convergence
• waybel29: The Characterization of Continuity of Topologies
• waybel30: Meet Continuous Lattices Revisited
• waybel31: Weights of Continuous Lattices
• waybel32: On the Order-consistent Topology of Complete and Uncomplete Lattices
• waybel33: Compactness of Lim-inf Topology
• waybel34: Duality Based on Galois Connection. Part I
• waybel35: Morphisms Into Chains, Part {I}
• waybel_0: Directed Sets, Nets, Ideals, Filters, and Maps
• waybel_1: Galois Connections
• waybel_2: Meet-continuous Lattices
• waybel_3: The "Way-Below" Relation
• waybel_4: Auxiliary and Approximating Relations
• waybel_5: The Equational Characterization of Continuous Lattices
• waybel_6: Irreducible and Prime Elements
• waybel_7: Prime Ideals and Filters
• waybel_8: Algebraic Lattices
• waybel_9: On The Topological Properties of Meet-Continuous Lattices
• weddwitt: Witt's Proof of the {W}edderburn Theorem
• weierstr: The Theorem of Weierstrass
• wellfnd1: On same equivalents of well-foundedness
• wellord1: The Well Ordering Relations
• wellord2: Zermelo Theorem and Axiom of Choice. The correspondence of well ordering relations and ordinal numbers
• wellset1: Zermelo's Theorem
• wsierp_1: The Chinese Remainder Theorem
• xboole_0: Boolean Properties of Sets - Definitions
• xboole_1: Boolean Properties of Sets - Theorems
• xboolean: On the Arithmetic of Boolean Values
• xcmplx_0: Complex Numbers - Basic Definitions
• xcmplx_1: Complex Numbers - Basic Theorems
• xfamily: Families of Subsets
• xreal_0: Introduction to Arithmetic of Real Numbers
• xreal_1: Real Numbers - Basic Theorems
• xregular: Consequences of Regularity Axiom
• xtuple_0: Kuratowski Pairs. {T}uples and Projections
• xxreal_0: Introduction to Arithmetic of Extended Real Numbers
• xxreal_1: Basic Properties of Extended Real Numbers
• xxreal_2: Suprema and Infima of Intervals of Extended Real Numbers
• xxreal_3: Basic Operations on Extended Real Numbers
• yellow10: The Properties of Product of Relational Structures
• yellow11: On the Characterization of Modular and Distributive Lattices
• yellow12: On the Characterization of {H}ausdorff Spaces
• yellow13: Introduction to Meet-Continuous Topological Lattices
• yellow14: Some Properties of Isomorphism between Relational Structures. On the Product of Topological Spaces
• yellow15: Components and Basis of Topological Spaces
• yellow16: Retracts and Inheritance
• yellow17: The Tichonov Theorem
• yellow18: Concrete Categories
• yellow19: On the characterizations of compactness
• yellow20: Miscellaneous Facts about Functors
• yellow21: Categorial Background for Duality Theory
• yellow_0: Bounds in Posets and Relational Substructures
• yellow_1: Boolean Posets, Posets under Inclusion and Products of Relational Structures
• yellow_2: Properties of Relational Structures, Posets, Lattices and Maps
• yellow_3: Cartesian Products of Relations and Relational Structures
• yellow_4: Definitions and Properties of the Join and Meet of Subsets
• yellow_5: Miscellaneous Facts about Relation Structure
• yellow_6: Moore-Smith Convergence
• yellow_7: Duality in Relation Structures
• yellow_8: Baire Spaces, Sober Spaces
• yellow_9: Bases and Refinements of Topologies
• yoneda_1: Yoneda Embedding
• zf_colla: The Contraction Lemma
• zf_fund1: Mostowski's Fundamental Operations - Part I
• zf_fund2: Mostowski's Fundamental Operations - Part II
• zf_lang: A Model of ZF Set Theory Language
• zf_lang1: Replacing of Variables in Formulas of ZF Theory
• zf_model: Models and Satisfiability. Defining by Structural Induction and Free Variables in ZF-formulae
• zf_refle: The Reflection Theorem
• zfmisc_1: Some Basic Properties of Sets
• zfmodel1: Properties of ZF Models
• zfmodel2: Definable Functions
• zfrefle1: Consequences of the Reflection Theorem
• zmatrlin: Matrix of $\mathbb Z$-module
• zmodlat1: Lattice of $\mathbb Z$-module
• zmodlat2: Embedded Lattice and Properties of {G}ram Matrix
• zmodlat3: Dual Lattice of $\mathbb Z$-module Lattice
• zmodul01: $\mathbb Z$-modules
• zmodul02: Quotient Module of $\mathbb Z$-module
• zmodul03: Free $\mathbb Z$-module
• zmodul04: Submodule of free $\mathbb Z$-module
• zmodul05: Rank of Submodule, Linear Transformations and Linearly Independent Subsets of $\mathbb Z$-module
• zmodul06: Torsion $\mathbb Z$-module and Torsion-free $\mathbb Z$-module
• zmodul07: Torsion-part of $\mathbb Z$-module
• zmodul08: Divisible $\mathbb Z$-modules