Nuprl Lemma : fl1_wf

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


Proof




Definitions occuring in Statement :  fl1: (x=1) face_lattice: face_lattice(I) names: names(I) lattice-point: Point(l) fset: fset(T) nat: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  face_lattice: face_lattice(I) uall: [x:A]. B[x] member: t ∈ T fl1: (x=1)
Lemmas referenced :  face-lattice1_wf names_wf names-deq_wf fset_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:names(I)].    ((x=1)  \mmember{}  Point(face\_lattice(I)))



Date html generated: 2016_05_18-PM-00_09_37
Last ObjectModification: 2015_12_28-PM-03_02_17

Theory : cubical!type!theory


Home Index