Nuprl Definition : in-hull
ij ∈ Hull(xs) == ∀k:ℕ||xs||. ((¬(k = i ∈ ℤ)) ⇒ (¬(k = j ∈ ℤ)) ⇒ (↑k L ij))
Definitions occuring in Statement :
left-test: i L jk,
length: ||as||,
int_seg: {i..j-},
assert: ↑b,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
length: ||as||,
implies: P ⇒ Q,
not: ¬A,
equal: s = t ∈ T,
int: ℤ,
assert: ↑b,
left-test: i L jk
FDL editor aliases :
in-hull
Latex:
ij \mmember{} Hull(xs) == \mforall{}k:\mBbbN{}||xs||. ((\mneg{}(k = i)) {}\mRightarrow{} (\mneg{}(k = j)) {}\mRightarrow{} (\muparrow{}k L ij))
Date html generated:
2017_10_02-PM-06_51_34
Last ObjectModification:
2017_08_06-PM-07_31_20
Theory : euclidean!plane!geometry
Home
Index