Nuprl Definition : Sierpinski
Sierpinski == f,g:ℕ ⟶ 𝔹//(f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))
Definitions occuring in Statement :
Sierpinski-bottom: ⊥,
quotient: x,y:A//B[x; y],
nat: ℕ,
bool: 𝔹,
iff: P ⇐⇒ Q,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
quotient: x,y:A//B[x; y],
iff: P ⇐⇒ Q,
equal: s = t ∈ T,
function: x:A ⟶ B[x],
nat: ℕ,
bool: 𝔹,
Sierpinski-bottom: ⊥
FDL editor aliases :
Sierpinski
Latex:
Sierpinski == f,g:\mBbbN{} {}\mrightarrow{} \mBbbB{}//(f = \mbot{} \mLeftarrow{}{}\mRightarrow{} g = \mbot{})
Date html generated:
2019_10_31-AM-06_35_24
Last ObjectModification:
2015_09_23-AM-09_28_54
Theory : synthetic!topology
Home
Index