Nuprl Lemma : dM0-sq-empty

[I:Top]. (0 {})


Proof




Definitions occuring in Statement :  dM0: 0 empty-fset: {} uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T dM0: 0 lattice-0: 0 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 empty-fset: {} nil: [] it:
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule hypothesis sqequalAxiom lemma_by_obid

Latex:
\mforall{}[I:Top].  (0  \msim{}  \{\})



Date html generated: 2016_05_18-AM-11_56_38
Last ObjectModification: 2015_12_28-PM-03_08_38

Theory : cubical!type!theory


Home Index