User:Jon Awbrey/SYMBOL
Formula Help
Bytes & Parses
· | · |
⋅ | ⋅ |
• | • |
∗ | ∗ |
◊ | ◊ |
{{unicode|·}} | Template:Unicode |
{{unicode|⋅}} | Template:Unicode |
{{unicode|•}} | Template:Unicode |
{{unicode|∗}} | Template:Unicode |
{{unicode|◊}} | Template:Unicode |
\(\cdot\) | \(\cdot\) |
\(\cdot\!\) | \(\cdot\!\) |
∈ | ∈ |
ε | ε |
\(\in\) | \(\in\) |
\(\in\!\) | \(\in\!\) |
\(\epsilon\) | \(\epsilon\) |
\(\epsilon\!\) | \(\epsilon\!\) |
\(\varepsilon\) | \(\varepsilon\) |
\(\varepsilon\!\) | \(\varepsilon\!\) |
η | η |
\(\eta\) | \(\eta\) |
\(\eta\!\) | \(\eta\!\) |
θ | θ |
\(\theta\) | \(\theta\) |
\(\theta\!\) | \(\theta\!\) |
\(\vartheta\) | \(\vartheta\) |
\(\vartheta\!\) | \(\vartheta\!\) |
χ | χ |
\(\chi\) | \(\chi\) |
\(\chi\!\) | \(\chi\!\) |
x = xJ = ¢(J) = J¢ = J ¢ = J¢ = J ¢
x = xJ = ¢(J) = J¢ = J ¢ = J¢ = J ¢
Display
New
W : ( [ Bn ] → [ Bk ] ) → ( [ Bn × Dn ] → [ Bk × Dk ] ) .
Concrete type \(\epsilon\) : ( U• → X• ) → ( EU• → X• ) Abstract type \(\epsilon\) : ( [Bn] → [Bk] ) → ( [Bn × Dn] → [Bk] )
Concrete type W : ( U• → X• ) → ( EU• → dX• ) Abstract type W : ( [Bn] → [Bk] ) → ( [Bn × Dn] → [Dk] )
\(\epsilon\)F : ( EU• → X• ⊆ EX• ) \(\cong\) ( [Bn × Dn] → [Bk] ⊆ [Bk × Dk] ) WF : ( EU• → dX• ⊆ EX• ) \(\cong\) ( [Bn × Dn] → [Dk] ⊆ [Bk × Dk] )
Old
W : ( [ Bn ] → [ Bk ] ) → ( [ Bn × Dn ] → [ Bk × Dk ] ) .
Concrete type \(\epsilon\) : ( U• → X• ) → ( EU• → X• ) Abstract type \(\epsilon\) : ( [Bn] → [Bk] ) → ( [Bn × Dn] → [Bk] )
Concrete type W : ( U• → X• ) → ( EU• → dX• ) Abstract type W : ( [Bn] → [Bk] ) → ( [Bn × Dn] → [Dk] )
\(\epsilon\)F : ( EU• → X• ⊆ EX• ) \(\cong\) ( [Bn × Dn] → [Bk] ⊆ [Bk × Dk] ) WF : ( EU• → dX• ⊆ EX• ) \(\cong\) ( [Bn × Dn] → [Dk] ⊆ [Bk × Dk] )
Epitext
Rosebud |
Rosebud |
Rosebud |
Gallery
’
`´
′
‹ ›
〈 〉
( )
( , )
A = {ai} = {a1, …, an} |
A = 〈A〉 = 〈a1, …, an〉= {‹a1, …, an›} |
A^ = (A → B) |
A• = [A] = [a1, …, an] |
dA = {dai} = {da1, …, dan} |
dA = 〈dA〉 = 〈da1, …, dan〉= {‹da1, …, dan›} |
dA^ = (dA → B) |
dA• = [dA] = [da1, …, dan] |
EA = A ∪ dA = {ai} ∪ {dai} = {a1, …, an, da1, …, dan} |
EA = 〈EA〉 = 〈a1, …, an, da1, …, dan〉= {‹a1, …, an, da1, …, dan›} |
EA^ = (EA → B) |
EA• = [EA] = [a1, …, an, da1, …, dan] |
X = {xi} = {x1, …, xn} |
X = 〈X〉 = 〈x1, …, xn〉= {‹x1, …, xn›} |
X^ = (X → B) |
X• = [X] = [x1, …, xn] |
dX = {dxi} = {dx1, …, dxn} |
dX = 〈dX〉 = 〈dx1, …, dxn〉= {‹dx1, …, dxn›} |
dX^ = (dX → B) |
dX• = [dX] = [dx1, …, dxn] |
X = {xi} = {x1, …, xn} |
X = 〈X〉 = 〈x1, …, xn〉= {‹x1, …, xn›} |
X^ = (X → B) |
X• = [X] = [x1, …, xn] |
f : Bk → B
f : Bn → B
f–1
Pow(X) = 2X
Arbitrary | → | Bn → B | X → B |
Basic | ¸> | Bn ¸> B | X ¸> B |
Linear | +> | Bn +> B | X +> B |
Positive | ¥> | Bn ¥> B | X ¥> B |
Singular | ××> | Bn ××> B | X ××> B |
The linear propositions, {hom : Bn → B} = (Bn +> B), may be expressed as sums of the following form:
\[\textstyle \sum_{i=1}^n e_i = e_1 + \ldots + e_n \ \mbox{where} \ \forall_{i=1}^n \ e_i = a_i \ \mbox{or} \ e_i = 0.\]
The positive propositions, {pos : Bn → B} = (Bn ¥> B), may be expressed as products of the following form:
\[\textstyle \prod_{i=1}^n e_i = e_1 \cdot \ldots \cdot e_n \ \mbox{where} \ \forall_{i=1}^n \ e_i = a_i \ \mbox{or} \ e_i = 1.\]
The singular propositions, {x : Bn → B} = (Bn ××> B), may be expressed as products of the following form:
\[\textstyle \prod_{i=1}^n e_i = e_1 \cdot \ldots \cdot e_n \ \mbox{where} \ \forall_{i=1}^n \ e_i = a_i \ \mbox{or} \ e_i = (a_i) = \lnot a_i.\]
I = {1, …, n}.
J ⊆ I
J ⊆ I
AJ
AJ
lJ : Bk → B
\(\ell_J : \mathbb{B}^k \to \mathbb{B}\)
θ : (Kn → K) → K
\(\theta\) : (Kn → K) → K
\(\theta\!\) : (Kn → K) → K
\(\vartheta\) : (Kn → K) → K
\(\vartheta\!\) : (Kn → K) → K
\(\chi\!\) : X → \(\bigcup_x \ \chi_x\!\)
\(\chi\!\) : Kn → ((Kn → K) → K)
\(\chi\!\) : (Kn → K) → (Kn → K)
\(\cong\)
\(\lceil x \rceil\)
xi(x) | χ(x ∈ Li) | \(\lceil x \in L_i \rceil\) | Li(x) |
xi(x) | \(\chi (x \in L_i)\) | \(\lceil x \in L_i \rceil\) | Li(x) |
‹0, 0, 0› | ‹0, 0, 0› |
‹0, 0, 1› | ‹0, 0, 1› |
‹0, 1, 0› | ‹0, 1, 0› |
‹0, 1, 1› | ‹0, 1, 1› |
‹1, 0, 0› | ‹1, 0, 0› |
‹1, 0, 1› | ‹1, 0, 1› |
‹1, 1, 0› | ‹1, 1, 0› |
‹1, 1, 1› | ‹1, 1, 1› |