Nuprl Lemma : polymorphic-constant-base
∀[T:Type]. ∀f:Base ⟶ T. ∃t:T. ∀x:Base. ((f x) = t ∈ T) supposing mono(T) ∧ value-type(T)
Proof
Definitions occuring in Statement : 
mono: mono(T)
, 
value-type: value-type(T)
, 
uimplies: b supposing a
, 
uall: ∀[x:A]. B[x]
, 
all: ∀x:A. B[x]
, 
exists: ∃x:A. B[x]
, 
and: P ∧ Q
, 
apply: f a
, 
function: x:A ⟶ B[x]
, 
base: Base
, 
universe: Type
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
uimplies: b supposing a
, 
member: t ∈ T
, 
and: P ∧ Q
, 
mono: mono(T)
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
prop: ℙ
, 
value-type: value-type(T)
, 
has-value: (a)↓
, 
exists: ∃x:A. B[x]
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
is-above: is-above(T;a;z)
, 
cand: A c∧ B
, 
not: ¬A
, 
false: False
Lemmas referenced : 
is-above_wf, 
base_wf, 
equal-wf-base, 
all_wf, 
equal_wf, 
mono_wf, 
value-type_wf, 
bottom_diverge, 
exception-not-bottom, 
has-value_wf_base, 
is-exception_wf, 
sqle_wf_base, 
and_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
cut, 
introduction, 
sqequalRule, 
sqequalHypSubstitution, 
productElimination, 
thin, 
independent_pairEquality, 
lambdaEquality, 
dependent_functionElimination, 
hypothesisEquality, 
axiomEquality, 
hypothesis, 
extract_by_obid, 
isectElimination, 
cumulativity, 
isect_memberEquality, 
axiomSqleEquality, 
because_Cache, 
equalityTransitivity, 
equalitySymmetry, 
rename, 
lambdaFormation, 
dependent_pairFormation, 
applyEquality, 
functionExtensionality, 
baseClosed, 
functionEquality, 
productEquality, 
universeEquality, 
pointwiseFunctionalityForEquality, 
independent_functionElimination, 
baseApply, 
closedConclusion, 
independent_pairFormation, 
divergentSqle, 
sqleRule, 
sqleReflexivity, 
voidElimination, 
instantiate, 
dependent_set_memberEquality, 
applyLambdaEquality, 
setElimination
Latex:
\mforall{}[T:Type].  \mforall{}f:Base  {}\mrightarrow{}  T.  \mexists{}t:T.  \mforall{}x:Base.  ((f  x)  =  t)  supposing  mono(T)  \mwedge{}  value-type(T)
Date html generated:
2018_05_21-PM-01_11_34
Last ObjectModification:
2018_05_01-PM-04_36_47
Theory : num_thy_1
Home
Index