Nuprl Lemma : decdr-to-bool_wf

[T:Type]. ∀[A,B:T ⟶ ℙ]. ∀[d:x:T ⟶ (A[x] B[x])].  (bool(d) ∈ T ⟶ 𝔹)


Proof




Definitions occuring in Statement :  decdr-to-bool: bool(d) bool: 𝔹 uall: [x:A]. B[x] prop: so_apply: x[s] member: t ∈ T function: x:A ⟶ B[x] union: left right universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T so_apply: x[s] subtype_rel: A ⊆B prop: decdr-to-bool: bool(d) it: bfalse: ff btrue: tt ifthenelse: if then else fi  all: x:A. B[x] implies:  Q
Lemmas referenced :  subtype_rel_self btrue_wf bfalse_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut sqequalHypSubstitution hypothesis functionEquality hypothesisEquality unionEquality applyEquality thin sqequalRule instantiate introduction extract_by_obid isectElimination because_Cache cumulativity universeEquality lambdaEquality lambdaFormation equalityTransitivity equalitySymmetry unionElimination dependent_functionElimination independent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[A,B:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:x:T  {}\mrightarrow{}  (A[x]  +  B[x])].    (bool(d)  \mmember{}  T  {}\mrightarrow{}  \mBbbB{})



Date html generated: 2019_10_30-AM-07_36_05
Last ObjectModification: 2018_08_21-PM-02_01_15

Theory : reals


Home Index