Nuprl Lemma : fl0-not-1

[I:fset(ℕ)]. ∀[x:names(I)].  ((x=0) 1 ∈ Point(face_lattice(I))))


Proof




Definitions occuring in Statement :  fl0: (x=0) face_lattice: face_lattice(I) names: names(I) lattice-1: 1 lattice-point: Point(l) fset: fset(T) nat: uall: [x:A]. B[x] not: ¬A equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T not: ¬A implies:  Q false: False face_lattice: face_lattice(I) lattice-1: 1 fl0: (x=0) face-lattice: face-lattice(T;eq) face-lattice0: (x=0) free-dist-lattice-with-constraints: free-dist-lattice-with-constraints(T;eq;x.Cs[x]) lattice-point: Point(l) constrained-antichain-lattice: constrained-antichain-lattice(T;eq;P) mk-bounded-distributive-lattice: mk-bounded-distributive-lattice mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o) all: x:A. B[x] top: Top eq_atom: =a y ifthenelse: if then else fi  bfalse: ff btrue: tt squash: T prop: subtype_rel: A ⊆B bdd-distributive-lattice: BoundedDistributiveLattice so_lambda: λ2x.t[x] and: P ∧ Q so_apply: x[s] uimplies: supposing a uiff: uiff(P;Q)
Lemmas referenced :  rec_select_update_lemma equal_wf lattice-point_wf face_lattice_wf subtype_rel_set bounded-lattice-structure_wf lattice-structure_wf lattice-axioms_wf bounded-lattice-structure-subtype bounded-lattice-axioms_wf uall_wf lattice-meet_wf lattice-join_wf fl0_wf lattice-1_wf bdd-distributive-lattice_wf names_wf fset_wf nat_wf fset-singletons-equal deq-fset_wf union-deq_wf names-deq_wf fset-singleton_wf empty-fset_wf member-fset-singleton fset-member_wf mem_empty_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin sqequalHypSubstitution sqequalRule extract_by_obid dependent_functionElimination isect_memberEquality voidElimination voidEquality hypothesis applyLambdaEquality setElimination rename imageMemberEquality hypothesisEquality baseClosed imageElimination because_Cache independent_functionElimination isectElimination applyEquality instantiate lambdaEquality productEquality cumulativity universeEquality independent_isectElimination unionEquality inlEquality productElimination equalitySymmetry hyp_replacement

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:names(I)].    (\mneg{}((x=0)  =  1))



Date html generated: 2017_10_05-AM-01_10_50
Last ObjectModification: 2017_07_28-AM-09_29_52

Theory : cubical!type!theory


Home Index