Nuprl Lemma : r2-eu-prim_wf
r2-eu-prim() ∈ GeometryPrimitives
Proof
Definitions occuring in Statement :
r2-eu-prim: r2-eu-prim(),
geo-primitives: GeometryPrimitives,
member: t ∈ T
Definitions unfolded in proof :
r2-eu-prim: r2-eu-prim(),
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
Latex:
r2-eu-prim() \mmember{} GeometryPrimitives
Date html generated:
2020_05_20-PM-01_10_21
Last ObjectModification:
2019_12_11-AM-09_47_12
Theory : reals!model!euclidean!geometry
Home
Index