Category:Mizar Articles
Jump to navigation
Jump to search
(previous page) (next page)
Pages in category "Mizar Articles"
The following 200 pages are in this category, out of 580 total.
(previous page) (next page)A
- Definition:Accumulation Point/Set
- Aleph Zero equals Cardinality of Naturals
- Aleph Zero is less than Cardinality of 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 Infima Preserving Mapping is Upper Adjoint of Galois Connection/Lemma 1
- All Infima Preserving Mapping is Upper Adjoint of Galois Connection/Lemma 2
- 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 Section
- Auxiliary Relation is Congruent
- Auxiliary Relation is Transitive
- Axiom:Axiom of Approximation
- Axiom of Approximation in Up-Complete Semilattice
- Axiom: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
- 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 Section 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 Section is Upper Section
- 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 Section is Lower Section
- 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
- Correctness of Definition of Increasing Mappings Satisfying Inclusion in Lower Closure
- Countable iff Cardinality not greater than Aleph Zero
D
- Definition:Dense (Lattice Theory)/Element
- Definition:Dense (Lattice 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
- 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 Dense
- Empty Intersection iff Subset of Relative Complement
- Empty Set 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