Nuprl Lemma : stable_req
∀[x,y:ℝ]. Stable{x = y}
Proof
Definitions occuring in Statement :
req: x = y,
real: ℝ,
stable: Stable{P},
uall: ∀[x:A]. B[x]
Definitions unfolded in proof :
nat: ℕ,
so_apply: x[s],
so_lambda: λ2x.t[x],
prop: ℙ,
false: False,
implies: P ⇒ Q,
not: ¬A,
and: P ∧ Q,
le: A ≤ B,
or: P ∨ Q,
decidable: Dec(P),
subtype_rel: A ⊆r B,
real: ℝ,
all: ∀x:A. B[x],
uimplies: b supposing a,
stable: Stable{P},
member: t ∈ T,
uall: ∀[x:A]. B[x],
req: x = y,
guard: {T}
Latex:
\mforall{}[x,y:\mBbbR{}]. Stable\{x = y\}
Date html generated:
2020_05_20-AM-10_53_13
Last ObjectModification:
2020_01_03-AM-01_07_07
Theory : reals
Home
Index