Nuprl Lemma : r2-straightedge-compass-simple1
∀c,d,a:ℝ^2. ∀b:{b:ℝ^2| b ≠ a ∧ c_b_d} . (∃u:ℝ^2 [(cu=cd ∧ a_b_u ∧ (b ≠ d ⇒ b ≠ u))])
Proof
Definitions occuring in Statement :
rv-be: a_b_c,
real-vec-sep: a ≠ b,
rv-congruent: ab=cd,
real-vec: ℝ^n,
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
and: P ∧ Q,
uall: ∀[x:A]. B[x],
nat: ℕ,
le: A ≤ B,
less_than': less_than'(a;b),
not: ¬A,
implies: P ⇒ Q,
false: False,
prop: ℙ,
exists: ∃x:A. B[x],
sq_exists: ∃x:A [B[x]],
cand: A c∧ B,
sq_stable: SqStable(P),
squash: ↓T,
rv-congruent: ab=cd,
subtype_rel: A ⊆r B,
real-vec-sep: a ≠ b,
uimplies: b supposing a,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q
Latex:
\mforall{}c,d,a:\mBbbR{}\^{}2. \mforall{}b:\{b:\mBbbR{}\^{}2| b \mneq{} a \mwedge{} c\_b\_d\} . (\mexists{}u:\mBbbR{}\^{}2 [(cu=cd \mwedge{} a\_b\_u \mwedge{} (b \mneq{} d {}\mRightarrow{} b \mneq{} u))])
Date html generated:
2020_05_20-PM-00_58_11
Last ObjectModification:
2019_12_11-PM-00_26_00
Theory : reals
Home
Index