Nuprl Lemma : face-lattice0-is-inc
∀T:Type. ∀eq:EqDecider(T). ∀x:T. ((x=0) ~ free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);inl x))
Proof
Definitions occuring in Statement :
face-lattice0: (x=0),
face-lattice-constraints: face-lattice-constraints(x),
free-dlwc-inc: free-dlwc-inc(eq;a.Cs[a];x),
union-deq: union-deq(A;B;a;b),
deq: EqDecider(T),
all: ∀x:A. B[x],
inl: inl x,
universe: Type,
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
face-lattice-constraints: face-lattice-constraints(x),
free-dlwc-inc: free-dlwc-inc(eq;a.Cs[a];x),
face-lattice0: (x=0),
fset-singleton: {x},
fset-filter: {x ∈ s | P[x]},
fset-null: fset-null(s),
member: t ∈ T,
top: Top,
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
sq_type: SQType(T),
implies: P ⇒ Q,
guard: {T},
ifthenelse: if b then t else f fi ,
bfalse: ff,
btrue: tt,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
and: P ∧ Q,
prop: ℙ,
uiff: uiff(P;Q),
not: ¬A,
f-subset: xs ⊆ ys,
isl: isl(x),
false: False,
or: P ∨ Q,
rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :
filter_cons_lemma,
filter_nil_lemma,
subtype_base_sq,
bool_subtype_base,
null_nil_lemma,
deq_wf,
eqff_to_assert,
deq-f-subset_wf,
union-deq_wf,
fset_wf,
bool_wf,
all_wf,
iff_wf,
f-subset_wf,
assert_wf,
fset-pair_wf,
fset-singleton_wf,
bnot_wf,
not_wf,
iff_transitivity,
iff_weakening_uiff,
assert_of_bnot,
assert-deq-f-subset,
member-fset-singleton,
btrue_wf,
and_wf,
equal_wf,
isl_wf,
bfalse_wf,
btrue_neq_bfalse,
member-fset-pair
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalRule,
lemma_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
isect_memberEquality,
voidElimination,
voidEquality,
hypothesis,
instantiate,
isectElimination,
because_Cache,
independent_isectElimination,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
hypothesisEquality,
universeEquality,
inlEquality,
inrEquality,
applyEquality,
unionEquality,
lambdaEquality,
setElimination,
rename,
setEquality,
functionEquality,
productElimination,
independent_pairFormation,
impliesFunctionality,
dependent_set_memberEquality,
inrFormation
Latex:
\mforall{}T:Type. \mforall{}eq:EqDecider(T). \mforall{}x:T.
((x=0) \msim{} free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);inl x))
Date html generated:
2020_05_20-AM-08_50_48
Last ObjectModification:
2015_12_28-PM-01_57_55
Theory : lattices
Home
Index