Nuprl Lemma : fl_all-0
∀I,J,i:Top. ((∀i.0) ~ 0)
Proof
Definitions occuring in Statement :
fl_all: (∀i.phi),
face_lattice: face_lattice(I),
lattice-0: 0,
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
fl_all: (∀i.phi),
fl-all-hom: fl-all-hom(I;i),
fl-lift: fl-lift(T;eq;L;eqL;f0;f1),
face-lattice-property,
free-dist-lattice-with-constraints-property,
lattice-extend-wc: lattice-extend-wc(L;eq;eqL;f;ac),
lattice-extend: lattice-extend(L;eq;eqL;f;ac),
lattice-fset-join: \/(s),
reduce: reduce(f;k;as),
list_ind: list_ind,
fset-image: f"(s),
f-union: f-union(domeq;rngeq;s;x.g[x]),
list_accum: list_accum,
lattice-0: 0,
record-select: r.x,
face_lattice: face_lattice(I),
face-lattice: face-lattice(T;eq),
free-dist-lattice-with-constraints: free-dist-lattice-with-constraints(T;eq;x.Cs[x]),
constrained-antichain-lattice: constrained-antichain-lattice(T;eq;P),
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice,
mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o),
record-update: r[x := v],
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
bfalse: ff,
btrue: tt,
empty-fset: {},
nil: [],
it: ⋅,
member: t ∈ T
Lemmas referenced :
face-lattice-property,
free-dist-lattice-with-constraints-property,
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalRule,
hypothesis,
lemma_by_obid
Latex:
\mforall{}I,J,i:Top. ((\mforall{}i.0) \msim{} 0)
Date html generated:
2016_05_18-PM-00_17_54
Last ObjectModification:
2016_03_25-PM-04_04_34
Theory : cubical!type!theory
Home
Index