### Nuprl Lemma : poset-cat-dist-non-zero

`∀[I:Cname List]. ∀[x,y:cat-ob(poset-cat(I))].`
`  (null(filter(λx1.((x x1 =z 0) ∧b (y x1 =z 1));I)) ~ ff) supposing `
`     ((¬(x = y ∈ cat-ob(poset-cat(I)))) and `
`     (cat-arrow(poset-cat(I)) x y))`

Proof

Definitions occuring in Statement :  poset-cat: `poset-cat(J)` coordinate_name: `Cname` cat-arrow: `cat-arrow(C)` cat-ob: `cat-ob(C)` null: `null(as)` filter: `filter(P;l)` list: `T List` band: `p ∧b q` eq_int: `(i =z j)` bfalse: `ff` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` apply: `f a` lambda: `λx.A[x]` natural_number: `\$n` sqequal: `s ~ t` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` uiff: `uiff(P;Q)` and: `P ∧ Q` prop: `ℙ` subtype_rel: `A ⊆r B` nat: `ℕ` poset-cat-dist: `poset-cat-dist(I;x;y)` all: `∀x:A. B[x]` cat-ob: `cat-ob(C)` pi1: `fst(t)` poset-cat: `poset-cat(J)` name-morph: `name-morph(I;J)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` nameset: `nameset(L)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` band: `p ∧b q` ifthenelse: `if b then t else f fi ` bfalse: `ff` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` false: `False` cons: `[a / b]`
Lemmas referenced :  poset-cat-dist-zero le_wf poset-cat-dist_wf nat_wf not_wf equal_wf cat-ob_wf poset-cat_wf cat-arrow_wf list_wf coordinate_name_wf filter_wf5 l_member_wf eq_int_wf nameset_wf extd-nameset_wf nil_wf all_wf assert_wf isname_wf bool_wf eqtt_to_assert assert_of_eq_int extd-nameset_subtype_int list-cases length_of_nil_lemma null_nil_lemma satisfiable-full-omega-tt intformnot_wf intformle_wf itermConstant_wf int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_formula_prop_wf product_subtype_list length_of_cons_lemma null_cons_lemma length_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination lambdaFormation independent_functionElimination productElimination applyEquality lambdaEquality setElimination rename sqequalRule natural_numberEquality promote_hyp sqequalAxiom isect_memberEquality equalityTransitivity equalitySymmetry setEquality functionEquality because_Cache functionExtensionality dependent_set_memberEquality unionElimination equalityElimination dependent_functionElimination dependent_pairFormation intEquality voidElimination voidEquality computeAll hypothesis_subsumption addEquality

Latex:
\mforall{}[I:Cname  List].  \mforall{}[x,y:cat-ob(poset-cat(I))].
(null(filter(\mlambda{}x1.((x  x1  =\msubz{}  0)  \mwedge{}\msubb{}  (y  x1  =\msubz{}  1));I))  \msim{}  ff)  supposing
((\mneg{}(x  =  y))  and
(cat-arrow(poset-cat(I))  x  y))

Date html generated: 2017_10_05-AM-10_28_47
Last ObjectModification: 2017_07_28-AM-11_23_50

Theory : cubical!sets

Home Index