Nuprl Lemma : req-same
∀[a:ℝ]. (a = a)
Proof
Definitions occuring in Statement :
req: x = y,
real: ℝ,
uall: ∀[x:A]. B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a
Latex:
\mforall{}[a:\mBbbR{}]. (a = a)
Date html generated:
2020_05_20-AM-10_53_19
Last ObjectModification:
2019_12_15-PM-06_41_12
Theory : reals
Home
Index