Nuprl Definition : TarskiPP
TarskiPP(e) == ∀a,b,c,d,t:Point. (((a_d_t ∧ b_d_c) ∧ a ≠ d) ⇒ (∃x,y:Point. ((a_b_x ∧ a_c_y) ∧ x_t_y)))
Definitions occuring in Statement :
geo-between: a_b_c,
geo-sep: a ≠ b,
geo-point: Point,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
geo-sep: a ≠ b,
exists: ∃x:A. B[x],
geo-point: Point,
and: P ∧ Q,
geo-between: a_b_c
FDL editor aliases :
TarskiPP
Latex:
TarskiPP(e) ==
\mforall{}a,b,c,d,t:Point. (((a\_d\_t \mwedge{} b\_d\_c) \mwedge{} a \mneq{} d) {}\mRightarrow{} (\mexists{}x,y:Point. ((a\_b\_x \mwedge{} a\_c\_y) \mwedge{} x\_t\_y)))
Date html generated:
2018_05_22-PM-00_14_40
Last ObjectModification:
2018_01_10-PM-01_22_39
Theory : euclidean!plane!geometry
Home
Index