Nuprl Lemma : mk-eu-prim_wf
∀[P:Type]. ∀[O:P ⟶ P ⟶ P ⟶ P ⟶ ℙ]. ∀[L:P ⟶ P ⟶ P ⟶ ℙ]. (Point=P O=O Left=L ∈ GeometryPrimitives)
Proof
Definitions occuring in Statement :
mk-eu-prim: mk-eu-prim,
geo-primitives: GeometryPrimitives,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
mk-eu-prim: mk-eu-prim,
geo-primitives: GeometryPrimitives,
geo-point: Point,
record+: record+,
record-update: r[x := v],
record: record(x.T[x]),
all: ∀x:A. B[x],
implies: P ⇒ Q,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
subtype_rel: A ⊆r B,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
ifthenelse: if b then t else f fi ,
sq_type: SQType(T),
guard: {T},
record-select: r.x,
top: Top,
eq_atom: x =a y,
bfalse: ff,
iff: P ⇐⇒ Q,
not: ¬A,
rev_implies: P ⇐ Q,
false: False,
prop: ℙ
Latex:
\mforall{}[P:Type]. \mforall{}[O:P {}\mrightarrow{} P {}\mrightarrow{} P {}\mrightarrow{} P {}\mrightarrow{} \mBbbP{}]. \mforall{}[L:P {}\mrightarrow{} P {}\mrightarrow{} P {}\mrightarrow{} \mBbbP{}].
(Point=P
O=O
Left=L \mmember{} GeometryPrimitives)
Date html generated:
2020_05_20-AM-09_41_11
Last ObjectModification:
2019_12_11-AM-09_44_08
Theory : euclidean!plane!geometry
Home
Index