Nuprl Lemma : in-hull-sorted
∀g:OrientedPlane. ∀xs:{xs:Point List| geo-general-position(g;xs)} . ∀i,j:ℕ||xs||.
((¬(i = j ∈ ℤ))
⇒ ij ∈ Hull(xs)
⇒ (∃ps:{k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List
(permutation({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} ;ps;
filter(λk.((¬b(k =z i)) ∧b (¬b(k =z j)));upto(||xs||)))
∧ sorted-by(λx,y. ((¬(x = y ∈ ℤ)) ⇒ (↑x L yi));ps))))
Proof
Definitions occuring in Statement :
in-hull: ij ∈ Hull(xs),
left-test: i L jk,
geo-general-position: geo-general-position(g;xs),
oriented-plane: OrientedPlane,
geo-point: Point,
permutation: permutation(T;L1;L2),
upto: upto(n),
sorted-by: sorted-by(R;L),
length: ||as||,
filter: filter(P;l),
list: T List,
band: p ∧b q,
int_seg: {i..j-},
bnot: ¬bb,
assert: ↑b,
eq_int: (i =z j),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
lambda: λx.A[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
uimplies: b supposing a,
int_seg: {i..j-},
lelt: i ≤ j < k,
and: P ∧ Q,
le: A ≤ B,
less_than: a < b,
squash: ↓T,
or: P ∨ Q,
sq_type: SQType(T),
guard: {T},
uiff: uiff(P;Q),
exists: ∃x:A. B[x],
bnot: ¬bb,
ifthenelse: if b then t else f fi ,
btrue: tt,
assert: ↑b,
bfalse: ff,
false: False,
band: p ∧b q,
subtype_rel: A ⊆r B,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s],
not: ¬A,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
sq_stable: SqStable(P),
top: Top,
satisfiable_int_formula: satisfiable_int_formula(fmla),
cand: A c∧ B,
sorted-by: sorted-by(R;L),
decidable: Dec(P),
hull-cmp: hull-cmp(g;xs;i;j),
true: True,
nequal: a ≠ b ∈ T ,
less_than': less_than'(a;b),
it: ⋅,
unit: Unit,
bool: 𝔹
Latex:
\mforall{}g:OrientedPlane. \mforall{}xs:\{xs:Point List| geo-general-position(g;xs)\} . \mforall{}i,j:\mBbbN{}||xs||.
((\mneg{}(i = j))
{}\mRightarrow{} ij \mmember{} Hull(xs)
{}\mRightarrow{} (\mexists{}ps:\{k:\mBbbN{}||xs||| (\mneg{}(k = i)) \mwedge{} (\mneg{}(k = j))\} List
(permutation(\{k:\mBbbN{}||xs||| (\mneg{}(k = i)) \mwedge{} (\mneg{}(k = j))\} ;ps;
filter(\mlambda{}k.((\mneg{}\msubb{}(k =\msubz{} i)) \mwedge{}\msubb{} (\mneg{}\msubb{}(k =\msubz{} j)));upto(||xs||)))
\mwedge{} sorted-by(\mlambda{}x,y. ((\mneg{}(x = y)) {}\mRightarrow{} (\muparrow{}x L yi));ps))))
Date html generated:
2020_05_20-AM-10_02_53
Last ObjectModification:
2020_01_13-PM-03_51_03
Theory : euclidean!plane!geometry
Home
Index