Nuprl Lemma : bottom-sqle
∀[x:Top]. (⊥ ≤ x)
Proof
Definitions occuring in Statement :
bottom: ⊥,
uall: ∀[x:A]. B[x],
top: Top,
sqle: s ≤ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
not: ¬A,
implies: P ⇒ Q,
false: False
Lemmas referenced :
bottom_diverge,
exception-not-bottom,
has-value_wf_base,
is-exception_wf,
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
divergentSqle,
extract_by_obid,
sqequalHypSubstitution,
independent_functionElimination,
thin,
hypothesis,
voidElimination,
isectElimination,
baseClosed,
axiomSqleEquality
Latex:
\mforall{}[x:Top]. (\mbot{} \mleq{} x)
Date html generated:
2019_06_20-AM-11_20_38
Last ObjectModification:
2018_08_21-PM-10_43_05
Theory : call!by!value_1
Home
Index