Nuprl Lemma : fl-morph-face-lattice0

[J,I:fset(ℕ)]. ∀[f:J ⟶ I]. ∀[x:names(I)].  (((x=0))<f> dM-to-FL(J;¬(f x)) ∈ Point(face_lattice(J)))


Proof




Definitions occuring in Statement :  fl-morph: <f> dM-to-FL: dM-to-FL(I;z) face_lattice: face_lattice(I) names-hom: I ⟶ J names-deq: NamesDeq names: names(I) dm-neg: ¬(x) face-lattice0: (x=0) lattice-point: Point(l) fset: fset(T) nat: uall: [x:A]. B[x] apply: a equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T fl-morph: <f> names-hom: I ⟶ J subtype_rel: A ⊆B DeMorgan-algebra: DeMorganAlgebra so_lambda: λ2x.t[x] prop: and: P ∧ Q guard: {T} uimplies: supposing a so_apply: x[s] lattice-point: Point(l) record-select: r.x dM: dM(I) free-DeMorgan-algebra: free-DeMorgan-algebra(T;eq) mk-DeMorgan-algebra: mk-DeMorgan-algebra(L;n) record-update: r[x := v] ifthenelse: if then else fi  eq_atom: =a y bfalse: ff free-DeMorgan-lattice: free-DeMorgan-lattice(T;eq) free-dist-lattice: free-dist-lattice(T; eq) mk-bounded-distributive-lattice: mk-bounded-distributive-lattice mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o) btrue: tt bdd-distributive-lattice: BoundedDistributiveLattice all: x:A. B[x] squash: T true: True iff: ⇐⇒ Q rev_implies:  Q implies:  Q bounded-lattice-hom: Hom(l1;l2) lattice-hom: Hom(l1;l2)
Lemmas referenced :  fl-lift_wf names_wf names-deq_wf face_lattice_wf face_lattice-deq_wf dM-to-FL_wf dm-neg_wf subtype_rel-equal lattice-point_wf dM_wf subtype_rel_set DeMorgan-algebra-structure_wf lattice-structure_wf lattice-axioms_wf bounded-lattice-structure-subtype DeMorgan-algebra-structure-subtype subtype_rel_transitivity bounded-lattice-structure_wf bounded-lattice-axioms_wf uall_wf equal_wf lattice-meet_wf lattice-join_wf DeMorgan-algebra-axioms_wf free-DeMorgan-lattice_wf squash_wf true_wf dM-to-FL-neg2 lattice-0_wf bdd-distributive-lattice_wf iff_weakening_equal set_wf bounded-lattice-hom_wf face-lattice_wf all_wf face-lattice0_wf face-lattice1_wf names-hom_wf fset_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis because_Cache lambdaEquality applyEquality sqequalRule instantiate productEquality independent_isectElimination cumulativity universeEquality lambdaFormation imageElimination equalityTransitivity equalitySymmetry dependent_functionElimination setElimination rename natural_numberEquality imageMemberEquality baseClosed productElimination independent_functionElimination isect_memberEquality axiomEquality

Latex:
\mforall{}[J,I:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].  \mforall{}[x:names(I)].    (((x=0))<f>  =  dM-to-FL(J;\mneg{}(f  x)))



Date html generated: 2017_10_05-AM-01_13_31
Last ObjectModification: 2017_07_28-AM-09_31_00

Theory : cubical!type!theory


Home Index