Nuprl Lemma : rat-cube-sub-complex-polyhedron-subtype
∀[k:ℕ]. ∀[K:ℚCube(k) List]. ∀[P:{c:ℚCube(k)| (c ∈ K)} ⟶ 𝔹]. (|rat-cube-sub-complex(P;K)| ⊆r |K|)
Proof
Definitions occuring in Statement :
rat-cube-complex-polyhedron: |K|,
l_member: (x ∈ l),
list: T List,
nat: ℕ,
bool: 𝔹,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
rat-cube-sub-complex: rat-cube-sub-complex(P;L),
rational-cube: ℚCube(k)
Definitions unfolded in proof :
l_subset: l_subset(T;as;bs),
implies: P ⇒ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
all: ∀x:A. B[x],
prop: ℙ,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
rat-cube-sub-complex: rat-cube-sub-complex(P;L),
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
member_filter_2,
l_subset-l_contains,
istype-nat,
list_wf,
bool_wf,
l_member_wf,
rational-cube_wf,
filter_wf5,
rat-cube-complex-polyhedron-subtype
Rules used in proof :
because_Cache,
lambdaFormation_alt,
independent_functionElimination,
productElimination,
dependent_functionElimination,
inhabitedIsType,
isectIsTypeImplies,
isect_memberEquality_alt,
universeIsType,
setIsType,
functionIsType,
axiomEquality,
sqequalRule,
independent_isectElimination,
hypothesis,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
cut,
introduction,
isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[k:\mBbbN{}]. \mforall{}[K:\mBbbQ{}Cube(k) List]. \mforall{}[P:\{c:\mBbbQ{}Cube(k)| (c \mmember{} K)\} {}\mrightarrow{} \mBbbB{}]. (|rat-cube-sub-complex(P;K)| \msubseteq{}r |K|)
Date html generated:
2019_11_04-PM-04_44_07
Last ObjectModification:
2019_10_31-PM-10_40_51
Theory : real!vectors
Home
Index