Nuprl Lemma : poset-cat-arrow-filter-nil
∀I:Cname List. ∀J:nameset(I) List. ∀c1,c2:cat-ob(poset-cat(I)). ∀f:cat-arrow(poset-cat(I)) c1 c2.
  ((filter(λz.(c1 z =z c2 z);J) = [] ∈ ({x:nameset(J)| ↑(c1 x =z c2 x)}  List))
  
⇒ (∀j∈J.((c1 j) = 0 ∈ ℕ2) ∧ ((c2 j) = 1 ∈ ℕ2)))
Proof
Definitions occuring in Statement : 
poset-cat: poset-cat(J)
, 
nameset: nameset(L)
, 
coordinate_name: Cname
, 
cat-arrow: cat-arrow(C)
, 
cat-ob: cat-ob(C)
, 
l_all: (∀x∈L.P[x])
, 
filter: filter(P;l)
, 
nil: []
, 
list: T List
, 
int_seg: {i..j-}
, 
assert: ↑b
, 
eq_int: (i =z j)
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
and: P ∧ Q
, 
set: {x:A| B[x]} 
, 
apply: f a
, 
lambda: λx.A[x]
, 
natural_number: $n
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
member: t ∈ T
, 
uall: ∀[x:A]. B[x]
, 
subtype_rel: A ⊆r B
, 
uimplies: b supposing a
, 
nameset: nameset(L)
, 
l_member: (x ∈ l)
, 
exists: ∃x:A. B[x]
, 
cand: A c∧ B
, 
coordinate_name: Cname
, 
int_upper: {i...}
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
sq_type: SQType(T)
, 
implies: P 
⇒ Q
, 
guard: {T}
, 
nat: ℕ
, 
squash: ↓T
, 
sq_stable: SqStable(P)
, 
ge: i ≥ j 
, 
decidable: Dec(P)
, 
or: P ∨ Q
, 
not: ¬A
, 
satisfiable_int_formula: satisfiable_int_formula(fmla)
, 
false: False
, 
top: Top
, 
and: P ∧ Q
, 
prop: ℙ
, 
cat-ob: cat-ob(C)
, 
pi1: fst(t)
, 
poset-cat: poset-cat(J)
, 
name-morph: name-morph(I;J)
, 
respects-equality: respects-equality(S;T)
, 
l_all: (∀x∈L.P[x])
, 
int_seg: {i..j-}
, 
lelt: i ≤ j < k
, 
less_than: a < b
, 
uiff: uiff(P;Q)
Lemmas referenced : 
list_wf, 
nameset_wf, 
coordinate_name_wf, 
subtype_rel_list, 
subtype_base_sq, 
set_subtype_base, 
le_wf, 
istype-int, 
int_subtype_base, 
select_wf, 
sq_stable__le, 
nat_properties, 
decidable__le, 
full-omega-unsat, 
intformand_wf, 
intformnot_wf, 
intformle_wf, 
itermConstant_wf, 
itermVar_wf, 
int_formula_prop_and_lemma, 
istype-void, 
int_formula_prop_not_lemma, 
int_formula_prop_le_lemma, 
int_term_value_constant_lemma, 
int_term_value_var_lemma, 
int_formula_prop_wf, 
assert_wf, 
eq_int_wf, 
filter_wf5, 
extd-nameset_wf, 
nil_wf, 
istype-assert, 
isname_wf, 
l_member_wf, 
respects-equality-list, 
respects-equality-set, 
respects-equality-set-trivial2, 
cat-arrow_wf, 
poset-cat_wf, 
cat-ob_wf, 
int_seg_wf, 
length_wf, 
poset-cat-arrow-not-equal, 
int_seg_properties, 
decidable__lt, 
intformless_wf, 
int_formula_prop_less_lemma, 
equal_functionality_wrt_subtype_rel2, 
filter_is_nil_implies, 
list-subtype, 
neg_assert_of_eq_int, 
extd-nameset_subtype_int
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
lambdaFormation_alt, 
cut, 
universeIsType, 
introduction, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesisEquality, 
hypothesis, 
lambdaEquality_alt, 
applyEquality, 
independent_isectElimination, 
setElimination, 
rename, 
because_Cache, 
sqequalRule, 
productElimination, 
instantiate, 
cumulativity, 
intEquality, 
natural_numberEquality, 
dependent_functionElimination, 
equalityTransitivity, 
equalitySymmetry, 
independent_functionElimination, 
applyLambdaEquality, 
imageMemberEquality, 
baseClosed, 
imageElimination, 
unionElimination, 
approximateComputation, 
dependent_pairFormation_alt, 
int_eqEquality, 
isect_memberEquality_alt, 
voidElimination, 
independent_pairFormation, 
equalityIstype, 
setEquality, 
setIsType, 
functionIsType, 
sqequalBase, 
inhabitedIsType
Latex:
\mforall{}I:Cname  List.  \mforall{}J:nameset(I)  List.  \mforall{}c1,c2:cat-ob(poset-cat(I)).  \mforall{}f:cat-arrow(poset-cat(I))  c1  c2.
    ((filter(\mlambda{}z.(c1  z  =\msubz{}  c2  z);J)  =  [])  {}\mRightarrow{}  (\mforall{}j\mmember{}J.((c1  j)  =  0)  \mwedge{}  ((c2  j)  =  1)))
Date html generated:
2019_11_05-PM-00_31_50
Last ObjectModification:
2018_12_10-AM-09_22_27
Theory : cubical!sets
Home
Index