Nuprl Lemma : rmax-rneq
∀x,y,z,w:ℝ. (rmax(x;y) ≠ rmax(z;w) ⇒ (x ≠ z ∨ y ≠ w))
Proof
Definitions occuring in Statement :
rneq: x ≠ y,
rmax: rmax(x;y),
real: ℝ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
rneq: x ≠ y,
or: P ∨ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
prop: ℙ,
and: P ∧ Q,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q
Latex:
\mforall{}x,y,z,w:\mBbbR{}. (rmax(x;y) \mneq{} rmax(z;w) {}\mRightarrow{} (x \mneq{} z \mvee{} y \mneq{} w))
Date html generated:
2020_05_20-AM-10_58_33
Last ObjectModification:
2019_11_11-PM-09_06_45
Theory : reals
Home
Index