Nuprl Lemma : face-presheaf-restriction-1
∀[A,B:fset(ℕ)]. ∀[g:B ⟶ A]. (g(1) = 1 ∈ Point(face_lattice(B)))
Proof
Definitions occuring in Statement :
face-presheaf: 𝔽,
face_lattice: face_lattice(I),
cube-set-restriction: f(s),
names-hom: I ⟶ J,
lattice-1: 1,
lattice-point: Point(l),
fset: fset(T),
nat: ℕ,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
face-presheaf: 𝔽,
all: ∀x:A. B[x],
top: Top
Lemmas referenced :
names-hom_wf,
fset_wf,
nat_wf,
cube_set_restriction_pair_lemma,
fl-morph-1
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
hypothesis,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule,
isect_memberEquality,
axiomEquality,
because_Cache,
dependent_functionElimination,
voidElimination,
voidEquality
Latex:
\mforall{}[A,B:fset(\mBbbN{})]. \mforall{}[g:B {}\mrightarrow{} A]. (g(1) = 1)
Date html generated:
2018_05_23-AM-08_38_59
Last ObjectModification:
2018_05_20-PM-05_50_47
Theory : cubical!type!theory
Home
Index