### Nuprl Lemma : req-int

`∀[a,b:ℤ].  uiff(r(a) = r(b);a = b ∈ ℤ)`

Proof

Definitions occuring in Statement :  req: `x = y` int-to-real: `r(n)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` prop: `ℙ` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` less_than': `less_than'(a;b)` less_than: `a < b` nat_plus: `ℕ+` all: `∀x:A. B[x]` req: `x = y` int-to-real: `r(n)` top: `Top` subtract: `n - m` or: `P ∨ Q` decidable: `Dec(P)` not: `¬A` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` sq_type: `SQType(T)` ifthenelse: `if b then t else f fi ` btrue: `tt` bfalse: `ff`

Latex:
\mforall{}[a,b:\mBbbZ{}].    uiff(r(a)  =  r(b);a  =  b)

Date html generated: 2020_05_20-AM-10_53_25
Last ObjectModification: 2020_01_06-PM-00_27_43

Theory : reals

Home Index