Nuprl Lemma : half-cubes-of_wf
∀[k:ℕ]. ∀[c:{c:ℚCube(k)| ↑Inhabited(c)} ].
(half-cubes-of(k;c) ∈ {L:ℚCube(k) List| no_repeats(ℚCube(k);L) ∧ (∀h:ℚCube(k). ((h ∈ L) ⇐⇒ ↑is-half-cube(k;h;c)))} )
Proof
Definitions occuring in Statement :
half-cubes-of: half-cubes-of(k;c),
inhabited-rat-cube: Inhabited(c),
is-half-cube: is-half-cube(k;h;c),
rational-cube: ℚCube(k),
no_repeats: no_repeats(T;l),
l_member: (x ∈ l),
list: T List,
nat: ℕ,
assert: ↑b,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]}
Definitions unfolded in proof :
half-cubes-of: half-cubes-of(k;c),
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
istype-nat,
rational-cube_wf,
inhabited-rat-cube_wf,
istype-assert,
half-cubes_wf
Rules used in proof :
inhabitedIsType,
isectIsTypeImplies,
isect_memberEquality_alt,
universeIsType,
setIsType,
equalitySymmetry,
equalityTransitivity,
axiomEquality,
dependent_set_memberEquality_alt,
hypothesis,
hypothesisEquality,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
applyEquality,
sqequalRule,
rename,
thin,
setElimination,
cut,
introduction,
isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[k:\mBbbN{}]. \mforall{}[c:\{c:\mBbbQ{}Cube(k)| \muparrow{}Inhabited(c)\} ].
(half-cubes-of(k;c) \mmember{} \{L:\mBbbQ{}Cube(k) List|
no\_repeats(\mBbbQ{}Cube(k);L)
\mwedge{} (\mforall{}h:\mBbbQ{}Cube(k). ((h \mmember{} L) \mLeftarrow{}{}\mRightarrow{} \muparrow{}is-half-cube(k;h;c)))\} )
Date html generated:
2019_10_29-AM-07_53_27
Last ObjectModification:
2019_10_21-PM-03_01_22
Theory : rationals
Home
Index