Nuprl Lemma : polymorphic-constant-bool

f:⋂A:Type. (A ⟶ 𝔹). ∃t:𝔹. ∀A:Type. ∀x:A.  t


Proof




Definitions occuring in Statement :  bool: 𝔹 all: x:A. B[x] exists: x:A. B[x] apply: a isect: x:A. B[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a and: P ∧ Q cand: c∧ B bool: 𝔹
Lemmas referenced :  polymorphic-constant bool_wf bool-mono union-value-type unit_wf2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis independent_isectElimination independent_pairFormation sqequalRule because_Cache dependent_functionElimination hypothesisEquality isectEquality universeEquality cumulativity functionEquality

Latex:
\mforall{}f:\mcap{}A:Type.  (A  {}\mrightarrow{}  \mBbbB{}).  \mexists{}t:\mBbbB{}.  \mforall{}A:Type.  \mforall{}x:A.    f  x  =  t



Date html generated: 2018_05_21-PM-01_11_44
Last ObjectModification: 2018_05_01-PM-04_36_54

Theory : num_thy_1


Home Index