Nuprl Lemma : r2-gt-or
∀a,b,c:ℝ^2. ∀d:{d:ℝ^2| d(c;d) < d(a;b)} . ∀x,y:ℝ^2.  ((d(c;d) < d(x;y)) ∨ (d(x;y) < d(a;b)))
Proof
Definitions occuring in Statement : 
real-vec-dist: d(x;y)
, 
real-vec: ℝ^n
, 
rless: x < y
, 
all: ∀x:A. B[x]
, 
or: P ∨ Q
, 
set: {x:A| B[x]} 
, 
natural_number: $n
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
member: t ∈ T
, 
uall: ∀[x:A]. B[x]
, 
nat: ℕ
, 
le: A ≤ B
, 
and: P ∧ Q
, 
less_than': less_than'(a;b)
, 
not: ¬A
, 
implies: P 
⇒ Q
, 
false: False
, 
subtype_rel: A ⊆r B
, 
prop: ℙ
Latex:
\mforall{}a,b,c:\mBbbR{}\^{}2.  \mforall{}d:\{d:\mBbbR{}\^{}2|  d(c;d)  <  d(a;b)\}  .  \mforall{}x,y:\mBbbR{}\^{}2.    ((d(c;d)  <  d(x;y))  \mvee{}  (d(x;y)  <  d(a;b)))
Date html generated:
2020_05_20-PM-01_10_29
Last ObjectModification:
2020_01_28-AM-10_59_48
Theory : reals!model!euclidean!geometry
Home
Index