Nuprl Lemma : extensional-real-to-bool-constant

āˆ€f:ā„ āŸ¶ š”¹. āˆ€x,y:ā„.  supposing āˆ€x,y:ā„.  ((x y) ā‡’ y)


Proof




Definitions occuring in Statement :  req: y real: ā„ bool: š”¹ uimplies: supposing a all: āˆ€x:A. B[x] implies: ā‡’ Q apply: a function: x:A āŸ¶ B[x] equal: t āˆˆ T
Definitions unfolded in proof :  all: āˆ€x:A. B[x] uimplies: supposing a member: t āˆˆ T decidable: Dec(P) or: P āˆØ Q not: Ā¬A implies: ā‡’ Q true: True false: False uall: āˆ€[x:A]. B[x] prop: ā„™ so_lambda: Ī»2x.t[x] guard: {T} sq_type: SQType(T) cand: cāˆ§ B and: P āˆ§ Q top: Top bfalse: ff btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) iff: ā‡ā‡’ Q

Latex:
\mforall{}f:\mBbbR{}  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x,y:\mBbbR{}.    f  x  =  f  y  supposing  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  f  x  =  f  y)



Date html generated: 2020_05_20-PM-00_05_12
Last ObjectModification: 2020_01_09-PM-06_15_14

Theory : reals


Home Index