Nuprl Definition : dual-plane-structure
DualPlaneStructure ==
DualPlanePrimitives
"Ssquashstable":∀x,y:Vec. SqStable((x # y))
"Pstable":∀x,y:Vec. Stable{(x ⊥ y)}
"SepOr":∀x:Vec. ∀y:{y:Vec| (x # y)} . ∀z:Vec. ((z # x) ∨ (z # y))
"cross":∀a:Vec. ∀b:{b:Vec| (a # b)} . (∃c:Vec [((a ⊥ c) ∧ (b ⊥ c))])
"nontrivial":∀a:Vec. (∃c:Vec [((a ⊥ c) ∧ (a # c))])
Definitions occuring in Statement :
dp-perp: (x ⊥ y),
dp-sep: (x # y),
dp-vec: Vec,
dual-plane-primitives: DualPlanePrimitives,
record+: record+,
sq_stable: SqStable(P),
stable: Stable{P},
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
token: "$token"
Definitions occuring in definition :
dp-sep: (x # y),
dp-perp: (x ⊥ y),
and: P ∧ Q,
dp-vec: Vec,
sq_exists: ∃x:A [B[x]],
all: ∀x:A. B[x],
token: "$token",
set: {x:A| B[x]} ,
or: P ∨ Q,
stable: Stable{P},
sq_stable: SqStable(P),
dual-plane-primitives: DualPlanePrimitives,
record+: record+
FDL editor aliases :
dual-plane-structure
Latex:
DualPlaneStructure ==
DualPlanePrimitives
"Ssquashstable":\mforall{}x,y:Vec. SqStable((x \# y))
"Pstable":\mforall{}x,y:Vec. Stable\{(x \mbot{} y)\}
"SepOr":\mforall{}x:Vec. \mforall{}y:\{y:Vec| (x \# y)\} . \mforall{}z:Vec. ((z \# x) \mvee{} (z \# y))
"cross":\mforall{}a:Vec. \mforall{}b:\{b:Vec| (a \# b)\} . (\mexists{}c:Vec [((a \mbot{} c) \mwedge{} (b \mbot{} c))])
"nontrivial":\mforall{}a:Vec. (\mexists{}c:Vec [((a \mbot{} c) \mwedge{} (a \# c))])
Date html generated:
2018_05_21-PM-09_44_42
Last ObjectModification:
2018_05_09-PM-01_59_25
Theory : matrices
Home
Index