Nuprl Lemma : polymorphic-constant

[T:Type]. ∀f:⋂A:Type. (A ⟶ T). ∃t:T. ∀A:Type. ∀x:A.  ((f x) t ∈ T) supposing mono(T) ∧ value-type(T)


Proof




Definitions occuring in Statement :  mono: mono(T) value-type: value-type(T) uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] and: P ∧ Q apply: a isect: x:A. B[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T and: P ∧ Q mono: mono(T) all: x:A. B[x] implies:  Q prop: value-type: value-type(T) has-value: (a)↓ cand: c∧ B exists: x:A. B[x] so_lambda: λ2x.t[x] subtype_rel: A ⊆B so_apply: x[s] squash: T true: True guard: {T} iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  is-above_wf base_wf equal-wf-base polymorphic-constant-base all_wf equal_wf mono_wf value-type_wf squash_wf true_wf iff_weakening_equal
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 independent_isectElimination independent_pairFormation dependent_pairFormation universeEquality instantiate applyEquality isectEquality functionEquality productEquality pointwiseFunctionalityForEquality imageElimination natural_numberEquality imageMemberEquality baseClosed independent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}f:\mcap{}A:Type.  (A  {}\mrightarrow{}  T).  \mexists{}t:T.  \mforall{}A:Type.  \mforall{}x:A.    ((f  x)  =  t)  supposing  mono(T)  \mwedge{}  value-type(T)



Date html generated: 2018_05_21-PM-01_11_39
Last ObjectModification: 2018_05_01-PM-04_36_51

Theory : num_thy_1


Home Index