Nuprl Lemma : pgeo-non-trivial-dual-ext
∀g:ProjectivePlane. (∃l:Line [l ≡ l])
Proof
Definitions occuring in Statement :
projective-plane: ProjectivePlane
,
pgeo-leq: a ≡ b
,
pgeo-line: Line
,
all: ∀x:A. B[x]
,
sq_exists: ∃x:A [B[x]]
Definitions unfolded in proof :
member: t ∈ T
,
point-exists-axiom: point-exists-axiom(g)
,
record-select: r.x
,
pgeo-three-lines: pgeo-three-line-axiom(p)
,
pi1: fst(t)
,
pgeo-non-trivial-dual,
pgeo-non-trivial,
pgeo-three-lines-axiom
Lemmas referenced :
pgeo-non-trivial-dual,
pgeo-non-trivial,
pgeo-three-lines-axiom
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}g:ProjectivePlane. (\mexists{}l:Line [l \mequiv{} l])
Date html generated:
2019_10_16-PM-02_12_38
Last ObjectModification:
2019_08_27-AM-08_39_14
Theory : euclidean!plane!geometry
Home
Index