# Category:Mizar Articles

## Pages in category "Mizar Articles"

The following 200 pages are in this category, out of 579 total.

(previous page) (next page)### A

- Definition:Accumulation Point of Set
- Aleph Zero equals Cardinality of Naturals
- Aleph Zero is less than Continuum
- Algebraic iff Continuous and For Every Way Below Exists Compact Between
- Definition:Algebraic Ordered Set
- All Infima Preserving Mapping is Upper Adjoint of Galois Connection
- All Suprema Preserving Mapping is Lower Adjoint of Galois Connection
- Definition:Approximating Relation
- Arithmetic iff Compact Subset form Lattice in Algebraic Lattice
- Arithmetic iff Way Below Relation is Multiplicative in Algebraic Lattice
- Definition:Arithmetic Ordered Set
- Auxiliary Approximating Relation has Interpolation Property
- Auxiliary Approximating Relation has Quasi Interpolation Property
- Definition:Auxiliary Relation
- Auxiliary Relation Image of Element is Upper Set
- Auxiliary Relation is Congruent
- Auxiliary Relation is Transitive
- Definition:Axiom of Approximation
- Axiom of Approximation in Up-Complete Semilattice
- Definition:Axiom of K-Approximation

### B

- Basis has Subset Basis of Cardinality equal to Weight of Space
- Bottom in Compact Subset
- Bottom in Ideal
- Bottom in Ordered Set of Topology
- Bottom is Compact
- Bottom is Way Below Any Element
- Bottom not in Proper Filter
- Bottom Relation is Auxiliary Relation
- Bottom Relation is Bottom in Ordered Set of Auxiliary Relations
- Boundary of Empty Set is Empty/Proof 1
- Boundary of Intersection is Subset of Union of Boundaries
- Boundary of Union is Subset of Union of Boundaries
- Boundary of Union of Separated Sets equals Union of Boundaries
- Brouwerian Lattice iff Meet-Continuous and Distributive
- Brouwerian Lattice iff Shift Mapping is Lower Adjoint
- Brouwerian Lattice is Distributive
- Brouwerian Lattice is Upper Bounded

### C

- Cardinalities form Inequality implies Difference is Nonempty
- Cardinality of Basis of Sorgenfrey Line not greater than Continuum
- Cardinality of Image of Mapping of Intersections is not greater than Weight of Space
- Cardinality of Image of Set not greater than Cardinality of Set
- Cardinality of Power Set is Invariant
- Cardinality of Set is Finite iff Set is Finite
- Cardinality of Set less than Cardinality of Power Set
- Cardinality of Set of Singletons
- Cardinality of Singleton
- Cardinality of Union not greater than Product
- Definition:Cartesian Product of Ordered Sets
- Cartesian Product of Ordered Sets is Ordered Set
- Chain is Directed
- Definition:Character of Point in Topological Space
- Definition:Character of Topological Space
- Characterization of Analytic Basis by Local Bases
- Characterization of Boundary by Basis
- Characterization of Boundary by Open Sets
- Characterization of Closure by Basis
- Characterization of Closure by Open Sets
- Characterization of Derivative by Local Basis
- Characterization of Derivative by Open Sets
- Characterization of Prime Element in Inclusion Ordered Set of Topology
- Characterization of Prime Element in Meet Semilattice
- Characterization of Prime Filter by Finite Suprema
- Characterization of Prime Ideal
- Characterization of Prime Ideal by Finite Infima
- Characterization of Pseudoprime Element by Finite Infima
- Characterization of Pseudoprime Element when Way Below Relation is Multiplicative
- Characterization of T0 Space by Closed Sets
- Characterization of T0 Space by Closures of Singletons
- Characterization of T0 Space by Distinct Closures of Singletons
- Closed Set iff Lower and Closed under Directed Suprema in Scott Topological Ordered Set
- Closed Subset is Upper in Lower Topology
- Definition:Closed under Directed Suprema
- Closure Equals Union with Derivative
- Closure of Dense-in-itself is Dense-in-itself in T1 Space
- Closure of Derivative is Derivative in T1 Space
- Closure of Set of Condensation Points equals Itself
- Closure of Singleton is Lower Closure of Element in Scott Topological Lattice
- Closure Operator does not Change Infimum of Subset of Image
- Closure Operator Preserves Directed Suprema iff Image of Closure Operator Inherits Directed Suprema
- Definition:Closure System
- Coarser Between Generator Set and Filter is Generator Set of Filter
- Definition:Coarser Subset (Order Theory)
- Definition:Compact Closure
- Compact Closure is Directed
- Compact Closure is Increasing
- Compact Closure is Intersection of Lower Closure and Compact Subset
- Compact Closure is Set of Finite Subsets in Lattice of Power Set
- Compact Closure is Subset of Way Below Closure
- Compact Closure of Element is Principal Ideal on Compact Subset iff Element is Compact
- Definition:Compact Element
- Compact Element iff Existence of Finite Subset that Element equals Intersection and Includes Subset
- Compact Element iff Principal Ideal
- Compact Subset is Bounded Below Join Semilattice
- Compact Subset is Join Subsemilattice
- Definition:Compact Subset of Lattice
- Complement of Closed under Directed Suprema Subset is Inaccessible by Directed Suprema
- Complement of Element is Irreducible implies Element is Meet Irreducible
- Complement of Inaccessible by Directed Suprema Subset is Closed under Directed Suprema
- Complement of Irreducible Topological Subset is Prime Element
- Complement of Lower Closure is Prime Element in Inclusion Ordered Set of Scott Sigma
- Complement of Lower Closure of Element is Open in Scott Topological Ordered Set
- Complement of Lower Set is Upper Set
- Complement of Subset with Property (S) is Closed under Directed Suprema
- Complement of Upper Closure of Element is Open in Lower Topology
- Complement of Upper Set is Lower Set
- Complete Lattice is Bounded
- Definition:Completely Irreducible
- Completely Irreducible and Subset Admits Infimum Equals Element implies Element Belongs to Subset
- Completely Irreducible Element equals Infimum of Subset implies Element Belongs to Subset
- Completely Irreducible Element iff Exists Element that Strictly Succeeds First Element
- Completely Irreducible implies Infimum differs from Element
- Completely Irreducible implies Meet Irreducible
- Composition of Galois Connections is Galois Connection
- Composition of Mapping and Inclusion is Restriction of Mapping
- Continuous iff Directed Suprema Preserving
- Continuous iff For Every Element There Exists Ideal Element Precedes Supremum
- Continuous iff Mapping at Element is Supremum
- Continuous iff Mapping at Element is Supremum of Compact Elements
- Continuous iff Mapping at Limit Inferior Precedes Limit Inferior of Composition of Mapping and Sequence
- Continuous iff Meet-Continuous and There Exists Smallest Auxiliary Approximating Relation
- Continuous iff Way Below Closure is Ideal and Element Precedes Supremum
- Continuous iff Way Below iff There Exists Element that Way Below and Way Below
- Continuous implies Increasing in Scott Topological Lattices
- Continuous Lattice and Way Below implies Preceding implies Preceding
- Continuous Lattice iff Auxiliary Approximating Relation is Superset of Way Below Relation
- Continuous Lattice is Meet-Continuous
- Definition:Continuous Lattice Subframe
- Continuous Lattice Subframe of Algebraic Lattice is Algebraic Lattice
- Definition:Continuous Ordered Set
- Continuum equals Cardinality of Power Set of Naturals
- Correctness of Definition of Increasing Mappings Satisfying Inclusion in Lower Closure
- Countable iff Cardinality not greater than Aleph Zero

### D

- Definition:Dense (Order Theory)/Element
- Definition:Dense (Order Theory)/Subset
- Density not greater than Weight
- Definition:Density of Topological Space
- Derivative is Included in Closure
- Derivative of Derivative is Subset of Derivative in T1 Space
- Derivative of Subset is Subset of Derivative
- Derivative of Union is Union of Derivatives
- Directed iff Filtered in Dual Ordered Set
- Directed iff Finite Subsets have Upper Bounds
- Directed iff Lower Closure Directed
- Directed in Join Semilattice
- Directed in Join Semilattice with Finite Suprema
- Definition:Directed Subset
- Definition:Directed Suprema Inheriting
- Directed Suprema Preserving Mapping at Element is Supremum
- Directed Suprema Preserving Mapping is Increasing
- Discrete Space is Separable iff Countable
- Down Mapping is Generated by Approximating Relation
- Dual Distributive Lattice is Distributive
- Dual of Dual Ordering
- Dual of Preordered Set is Preordered Set
- Dual Ordered Set is Ordered Set

### E

- Help:Editing/House Style
- Help:Editing/House Style/Sources
- Element equals to Supremum of Infima of Open Sets that Element Belongs implies Topological Lattice is Continuous
- Element is Finite iff Element is Compact in Lattice of Power Set
- Element is Meet Irreducible iff Complement of Element is Irreducible
- Definition:Element is Way Below
- Element of Increasing Mappings Satisfying Inclusion in Lower Closure is Generated by Auxiliary Relation
- Element of Ordered Set of Topology is Dense iff is Everywhere Debse
- Empty Intersection iff Subset of Relative Complement
- Empty is Bottom of Lattice of Power Set
- Equivalence of Definitions of Principal Ideal
- Every Element is Directed and Every Two Elements are Included in Third Element implies Union is Directed
- Every Element is Lower implies Union is Lower
- Every Pseudoprime Element is Prime implies Lattice is Arithmetic
- Existence of Non-Empty Finite Infima in Meet Semilattice
- Existence of Non-Empty Finite Suprema in Join Semilattice
- Existence of Subfamily of Cardinality not greater than Weight of Space and Unions Equal
- Extension of Directed Suprema Preserving Mapping to Complete Lattice Preserves Directed Suprema
- Extension of Infima Preserving Mapping to Complete Lattice Preserves Infima

### F

- Definition:Filter in Ordered Set
- Filter is Ideal in Dual Ordered Set
- Filter is Prime iff For Every Element Element either Negation Belongs to Filter in Boolean Lattice
- Filtered iff Directed in Dual Ordered Set
- Filtered iff Finite Subsets have Lower Bounds
- Filtered iff Upper Closure Filtered
- Filtered in Meet Semilattice
- Filtered in Meet Semilattice with Finite Infima
- Definition:Filtered Subset
- Filters equal Ideals in Dual Ordered Set
- Filters form Complete Lattice
- Filters of Lattice of Power Set form Bounded Above Ordered Set
- Filters of Lattice of Power Set form Bounded Below Ordered Set
- Definition:Finer Subset (Order Theory)
- Finer Supremum Precedes Supremum
- Finite iff Cardinality Less than Aleph Zero
- Definition:Finite Infima Set
- Finite Infima Set and Upper Closure is Filter
- Finite Infima Set and Upper Closure is Smallest Filter
- Finite Infima Set of Coarser Subset is Coarser than Finite Infima Set
- Finite Subset Bounds Element of Finite Infima Set and Upper Closure
- Finite Subset Bounds Element of Finite Suprema Set and Lower Closure
- Finite Subsets form Ideal
- Definition:Finite Suprema Set
- Finite Suprema Set and Lower Closure is Ideal
- Finite Suprema Set and Lower Closure is Smallest Ideal