Nuprl Lemma : P_point-apartness-relation1
∀e:EuclideanParPlane. ∀P:P_point(e). (¬P_point-sep(e;P;P))
Proof
Definitions occuring in Statement :
P_point-sep: P_point-sep(eu;P;Q),
P_point: P_point(eu),
euclidean-parallel-plane: EuclideanParPlane,
all: ∀x:A. B[x],
not: ¬A
Definitions unfolded in proof :
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
false: False,
P_point-sep: P_point-sep(eu;P;Q),
exists: ∃x:A. B[x],
and: P ∧ Q,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x]
Lemmas referenced :
P_point-sep_wf,
P_point_wf,
euclidean-parallel-plane_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
thin,
sqequalHypSubstitution,
productElimination,
independent_functionElimination,
hypothesis,
voidElimination,
because_Cache,
introduction,
extract_by_obid,
isectElimination,
hypothesisEquality,
dependent_functionElimination
Latex:
\mforall{}e:EuclideanParPlane. \mforall{}P:P\_point(e). (\mneg{}P\_point-sep(e;P;P))
Date html generated:
2019_10_16-PM-03_02_08
Last ObjectModification:
2018_08_19-PM-09_39_10
Theory : euclidean!plane!geometry
Home
Index