Nuprl Lemma : Sierpinski-bottom_wf
⊥ ∈ ℕ ⟶ 𝔹
Proof
Definitions occuring in Statement :
Sierpinski-bottom: ⊥,
nat: ℕ,
bool: 𝔹,
member: t ∈ T,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
Sierpinski-bottom: ⊥,
member: t ∈ T
Lemmas referenced :
bfalse_wf,
nat_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaEquality,
cut,
lemma_by_obid,
hypothesis
Latex:
\mbot{} \mmember{} \mBbbN{} {}\mrightarrow{} \mBbbB{}
Date html generated:
2019_10_31-AM-06_35_15
Last ObjectModification:
2015_12_28-AM-11_21_43
Theory : synthetic!topology
Home
Index