Nuprl Lemma : base-not-discrete
¬discrete-type(Base)
Proof
Definitions occuring in Statement :
discrete-type: discrete-type(T),
not: ¬A,
base: Base
Definitions unfolded in proof :
not: ¬A,
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
false: False,
prop: ℙ
Lemmas referenced :
strong-subtype-discrete-type,
partial_wf,
base_wf,
partial-strong-subtype-base,
int_subtype_base,
partial-int-not-discrete,
discrete-type_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
intEquality,
hypothesis,
independent_isectElimination,
because_Cache,
independent_functionElimination,
voidElimination
Latex:
\mneg{}discrete-type(Base)
Date html generated:
2018_05_22-PM-02_15_50
Last ObjectModification:
2017_10_30-PM-00_43_01
Theory : reals
Home
Index