Nuprl Lemma : pgeo-lpsep-dual
∀[p,l,b:Top]. (l ≠ b ~ l ≠ b)
Proof
Definitions occuring in Statement :
pgeo-lpsep: a ≠ b,
pgeo-dual-prim: pg*,
pgeo-plsep: a ≠ b,
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
pgeo-dual-prim: pg*,
pgeo-plsep: a ≠ b,
pgeo-lpsep: a ≠ b,
mk-pgeo-prim: mk-pgeo-prim,
all: ∀x:A. B[x],
top: Top,
eq_atom: x =a y,
ifthenelse: if b then t else f fi ,
btrue: tt
Lemmas referenced :
rec_select_update_lemma,
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
isect_memberEquality,
voidElimination,
voidEquality,
hypothesis,
sqequalAxiom,
isectElimination,
hypothesisEquality,
because_Cache
Latex:
\mforall{}[p,l,b:Top]. (l \mneq{} b \msim{} l \mneq{} b)
Date html generated:
2018_05_22-PM-00_25_11
Last ObjectModification:
2017_10_31-PM-01_56_30
Theory : euclidean!plane!geometry
Home
Index