Nuprl Lemma : metric-weak-Markov
∀[X:Type]. ∀d:metric(X). (mcomplete(X with d) ⇒ (∀x,y:X. ((∀z:X. ((¬z ≡ x) ∨ (¬z ≡ y))) ⇒ x # y)))
Proof
Definitions occuring in Statement :
mcomplete: mcomplete(M),
mk-metric-space: X with d,
msep: x # y,
meq: x ≡ y,
metric: metric(X),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
not: ¬A,
member: t ∈ T,
prop: ℙ,
false: False,
nat_plus: ℕ+,
uimplies: b supposing a,
rneq: x ≠ y,
guard: {T},
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
decidable: Dec(P),
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
rless: x < y,
sq_exists: ∃x:A [B[x]],
int_seg: {i..j-},
lelt: i ≤ j < k,
top: Top,
cand: A c∧ B,
sq_type: SQType(T),
true: True,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
nat: ℕ,
ge: i ≥ j ,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
cons: [a / b],
le: A ≤ B,
less_than': less_than'(a;b),
colength: colength(L),
nil: [],
it: ⋅,
less_than: a < b,
squash: ↓T,
upto: upto(n),
from-upto: [n, m),
lt_int: i <z j,
ifthenelse: if b then t else f fi ,
btrue: tt,
bfalse: ff,
bool: 𝔹,
unit: Unit,
uiff: uiff(P;Q),
bnot: ¬bb,
assert: ↑b,
mcomplete: mcomplete(M),
mk-metric-space: X with d,
mcauchy: mcauchy(d;n.x[n]),
eq_int: (i =z j),
rev_uimplies: rev_uimplies(P;Q),
real: ℝ,
sq_stable: SqStable(P),
rge: x ≥ y,
subtract: n - m,
mconverges: x[n]↓ as n→∞,
mconverges-to: lim n→∞.x[n] = y,
nequal: a ≠ b ∈ T ,
meq: x ≡ y,
mdist: mdist(d;x;y),
req_int_terms: t1 ≡ t2,
msep: x # y
Latex:
\mforall{}[X:Type]
\mforall{}d:metric(X). (mcomplete(X with d) {}\mRightarrow{} (\mforall{}x,y:X. ((\mforall{}z:X. ((\mneg{}z \mequiv{} x) \mvee{} (\mneg{}z \mequiv{} y))) {}\mRightarrow{} x \# y)))
Date html generated:
2020_05_20-AM-11_58_40
Last ObjectModification:
2020_01_03-PM-09_15_57
Theory : reals
Home
Index