Nuprl Definition : pgeo-finite-plane
pgeo-finite-plane(pg) == ((∃p_n:ℕ. Point ~ ℕp_n) ∧ (∃l_n:ℕ. Line ~ ℕl_n)) ∧ (∀p:Point. ∀l:Line. Dec(p ≠ l))
Definitions occuring in Statement :
pgeo-plsep: a ≠ b,
pgeo-line: Line,
pgeo-point: Point,
equipollent: A ~ B,
int_seg: {i..j-},
nat: ℕ,
decidable: Dec(P),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
natural_number: $n
Definitions occuring in definition :
and: P ∧ Q,
exists: ∃x:A. B[x],
nat: ℕ,
equipollent: A ~ B,
int_seg: {i..j-},
natural_number: $n,
pgeo-point: Point,
all: ∀x:A. B[x],
pgeo-line: Line,
decidable: Dec(P),
pgeo-plsep: a ≠ b
FDL editor aliases :
pgeo-finite-plane
Latex:
pgeo-finite-plane(pg) ==
((\mexists{}p$_{n}$:\mBbbN{}. Point \msim{} \mBbbN{}p$_{n}$) \mwedge{} (\mexists{}l$_{n}\000C$:\mBbbN{}. Line \msim{} \mBbbN{}l$_{n}$)) \mwedge{} (\mforall{}p:Point. \mforall{}l:Line. Dec(p \mneq{} l))
Date html generated:
2018_05_22-PM-00_59_20
Last ObjectModification:
2018_01_10-AM-09_56_32
Theory : euclidean!plane!geometry
Home
Index