Nuprl Lemma : req_fake_le_antisymmetry
∀[x,y:ℝ]. (x = y) supposing ((y ≤ x) and (x ≤ y))
Proof
Definitions occuring in Statement :
rleq: x ≤ y,
req: x = y,
real: ℝ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
guard: {T},
implies: P ⇒ Q,
prop: ℙ
Latex:
\mforall{}[x,y:\mBbbR{}]. (x = y) supposing ((y \mleq{} x) and (x \mleq{} y))
Date html generated:
2020_05_20-AM-10_57_05
Last ObjectModification:
2020_01_02-PM-02_13_43
Theory : reals
Home
Index