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