Nuprl Lemma : real-weak-Markov
∀x,y:ℝ. x ≠ y supposing ∀z:ℝ. ((¬(z = x)) ∨ (¬(z = y)))
Proof
Definitions occuring in Statement :
rneq: x ≠ y,
req: x = y,
real: ℝ,
uimplies: b supposing a,
all: ∀x:A. B[x],
not: ¬A,
or: P ∨ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x],
or: P ∨ Q,
not: ¬A,
implies: P ⇒ Q,
prop: ℙ,
false: False,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
uiff: uiff(P;Q),
req_int_terms: t1 ≡ t2,
rev_uimplies: rev_uimplies(P;Q),
stable: Stable{P},
rge: x ≥ y,
guard: {T}
Latex:
\mforall{}x,y:\mBbbR{}. x \mneq{} y supposing \mforall{}z:\mBbbR{}. ((\mneg{}(z = x)) \mvee{} (\mneg{}(z = y)))
Date html generated:
2020_05_20-AM-11_18_00
Last ObjectModification:
2020_01_03-PM-01_29_16
Theory : reals
Home
Index