Nuprl Lemma : dM_inc_wf

[I:fset(ℕ)]. ∀[x:names(I)].  (<x> ∈ Point(dM(I)))


Proof




Definitions occuring in Statement :  dM_inc: <x> dM: dM(I) names: names(I) lattice-point: Point(l) fset: fset(T) nat: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T dM_inc: <x> dM: dM(I) top: Top
Lemmas referenced :  free-dma-point dminc_wf names_wf names-deq_wf fset_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality voidElimination voidEquality hypothesis hypothesisEquality axiomEquality equalityTransitivity equalitySymmetry because_Cache

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:names(I)].    (<x>  \mmember{}  Point(dM(I)))



Date html generated: 2016_05_18-AM-11_56_31
Last ObjectModification: 2015_12_28-PM-03_09_00

Theory : cubical!type!theory


Home Index