Mizar articles

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