Example Uses of General Topology Entity Store

Initialization (compressed form of the entity store):
In[]:=
imstore=
;
In[]:=
myStore=ToExpression[StringJoin[FromCharacterCode[Take[Flatten[Round[ImageData[imstore]65535]],3131285]]]];​​PrependTo[$EntityStores,myStore];​​EntityValue["GeneralTopologyTheorem","Activate"]//Activate;​​EntityValue["GeneralTopologyTheorem","TraditionalFormMakeBoxAssignments"]//Activate;
Obtain lists of properties for theorems and concepts.
In[]:=
EntityValue["GeneralTopologyTheorem","Properties"]
Out[]=

qualifying objects
,
restrictions
,
statement
,
references
,
notation
,
alternate names
,
label
,
input form summary grid
,
summary grid
,
related concepts

In[]:=
EntityValue["GeneralTopologyConcept","Properties"]
Out[]=

arguments
,
restrictions
,
output
,
references
,
notation
,
alternate names
,
label
,
input form summary grid
,
summary grid
,
related concepts
,
related theorems

Obtain lists of concepts and theorems.
In[]:=
EntityList@"GeneralTopologyConcept"
Out[]=
In[]:=
EntityList@"GeneralTopologyTheorem"
Out[]=
Calculate the related theorems for a concept.
In[]:=
Entity["GeneralTopologyConcept","QuotientSpace"]["RelatedTheorems"]
Out[]=

surjective map is quotient map with respect to quotient topology
,
quotient space homeomorphic to quotient by fibers
,
Hausdorff criterion for space of fibers

View a summary grid for a theorem.
In[]:=
Entity["GeneralTopologyTheorem","ClassicalAscolisTheorem"]["SummaryGrid"]
Out[]=
Theorem
ClassicalAscolisTheorem
Label
classical Ascoli's Theorem
AlternateNames
MunkresTheorem45.4
QualifyingObjects
F,,n
Notation
X:>

el
d:>the Euclidean metric on
n

Restrictions
 is compact
F⊆
Hom
Top
(,
n

)
n∈
n>0
Statement
the family F of maps ⟶(
n

, d) is equicontinuousandthe family F of maps ⟶(
n

, d) is pointwise bounded⧦F is a precompact subset of
Hom
Top
(,
n

)⊆
X
(
n

)
with the uniform topology induced by d
References
James Munkres. Topology. pp. 278-279, 2000
RelatedConcepts
EuclideanMetric,IsCompact,EuclideanSpace,IsPrecompactSubsetOf,AsTopologicalSubspaceOf,SpaceWithUniformTopology,IsEquicontinuous,IsPointwiseBounded
Display usage messages for a symbol.
In[]:=
?Mapping
Mapping[X, Y, x ↦ f[x]] represents the function f: X -> Y.
Mapping[X, x ↦ f[x]] represents the function f: X -> f(X).
Mapping[SetBuilder[{
x
1
, …,
x
n
}], {
x
1
↦ f[
x
1
], …,
x
n
↦ f[
x
n
]}] represents a function on a finite set.
View expressions in traditional form.
In[]:=
SetBuilder[x^2,x∈Integers]//TraditionalForm
Out[]//TraditionalForm=
{
2
x
| x∈ }
In[]:=
Mapping[Reals,Integers,x↦Floor[x]]//TraditionalForm
Out[]//TraditionalForm=
∋x⌊x⌋∈
In[]:=
~Math["IsTopologicalSubspaceOf"]~//TraditionalForm
Out[]//TraditionalForm=
 is a topological subspace of 