Nuprl Lemma : real-weak-Markov-ext
∀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 :
member: t ∈ T,
real-weak-Markov,
rneq-if-rabs
Lemmas referenced :
real-weak-Markov,
rneq-if-rabs
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}x,y:\mBbbR{}. x \mneq{} y supposing \mforall{}z:\mBbbR{}. ((\mneg{}(z = x)) \mvee{} (\mneg{}(z = y)))
Date html generated:
2017_10_03-AM-09_10_17
Last ObjectModification:
2017_09_06-PM-05_53_13
Theory : reals
Home
Index