Nuprl Lemma : face_lattice-induction
∀I:fset(ℕ)
∀[P:Point(face_lattice(I)) ⟶ ℙ]
((∀x:Point(face_lattice(I)). SqStable(P[x]))
⇒ P[0]
⇒ P[1]
⇒ (∀x,y:Point(face_lattice(I)). (P[x] ⇒ P[y] ⇒ P[x ∨ y]))
⇒ (∀x:Point(face_lattice(I)). (P[x] ⇒ (∀i:names(I). (P[(i=0) ∧ x] ∧ P[(i=1) ∧ x]))))
⇒ {∀x:Point(face_lattice(I)). P[x]})
Proof
Definitions occuring in Statement :
fl1: (x=1),
fl0: (x=0),
face_lattice: face_lattice(I),
names: names(I),
lattice-0: 0,
lattice-1: 1,
lattice-join: a ∨ b,
lattice-meet: a ∧ b,
lattice-point: Point(l),
fset: fset(T),
nat: ℕ,
sq_stable: SqStable(P),
uall: ∀[x:A]. B[x],
prop: ℙ,
guard: {T},
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
all: ∀x:A. B[x],
face_lattice: face_lattice(I),
guard: {T},
fl1: (x=1),
fl0: (x=0),
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
nat_wf,
fset_wf,
names-deq_wf,
names_wf,
face-lattice-induction
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalRule,
cut,
lemma_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
isectElimination,
hypothesisEquality,
hypothesis
Latex:
\mforall{}I:fset(\mBbbN{})
\mforall{}[P:Point(face\_lattice(I)) {}\mrightarrow{} \mBbbP{}]
((\mforall{}x:Point(face\_lattice(I)). SqStable(P[x]))
{}\mRightarrow{} P[0]
{}\mRightarrow{} P[1]
{}\mRightarrow{} (\mforall{}x,y:Point(face\_lattice(I)). (P[x] {}\mRightarrow{} P[y] {}\mRightarrow{} P[x \mvee{} y]))
{}\mRightarrow{} (\mforall{}x:Point(face\_lattice(I)). (P[x] {}\mRightarrow{} (\mforall{}i:names(I). (P[(i=0) \mwedge{} x] \mwedge{} P[(i=1) \mwedge{} x]))))
{}\mRightarrow{} \{\mforall{}x:Point(face\_lattice(I)). P[x]\})
Date html generated:
2016_05_18-PM-00_11_22
Last ObjectModification:
2016_03_26-PM-00_03_27
Theory : cubical!type!theory
Home
Index