User:Jon Awbrey/SYMBOL
Formula Help
Bytes & Parses
| · | · |
| ⋅ | ⋅ |
| • | • |
| ∗ | ∗ |
| ◊ | ◊ |
| \(\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› |
