Nuprl Lemma : partition-point-member
∀I:Interval. (icompact(I) ⇒ (∀p:partition(I). (∀x∈p.x ∈ I)))
Proof
Definitions occuring in Statement :
partition: partition(I),
icompact: icompact(I),
i-member: r ∈ I,
interval: Interval,
l_all: (∀x∈L.P[x]),
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
partition: partition(I),
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
sq_stable: SqStable(P),
squash: ↓T,
l_all: (∀x∈L.P[x]),
uall: ∀[x:A]. B[x],
int_seg: {i..j-},
uimplies: b supposing a,
lelt: i ≤ j < k,
and: P ∧ Q,
le: A ≤ B,
less_than: a < b,
decidable: Dec(P),
or: P ∨ Q,
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
prop: ℙ,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
partitions: partitions(I;p),
rbetween: x≤y≤z,
icompact: icompact(I),
frs-non-dec: frs-non-dec(L),
rev_uimplies: rev_uimplies(P;Q),
less_than': less_than'(a;b),
rge: x ≥ y,
guard: {T},
last: last(L)
Latex:
\mforall{}I:Interval. (icompact(I) {}\mRightarrow{} (\mforall{}p:partition(I). (\mforall{}x\mmember{}p.x \mmember{} I)))
Date html generated:
2020_05_20-AM-11_36_37
Last ObjectModification:
2020_01_06-PM-00_18_30
Theory : reals
Home
Index