Nuprl Lemma : one-dimensional-dM
The free DeMorgan algebra with one generator i is the free distributive
lattice with two generators, i and 1-i. Hence it has exactly six elements.
The proof is somewhat tedious, but we need this lemma so that we
can prove that all paths in a "discrete cubical type" ⌜discr(T)⌝ are constant.⋅
∀i:ℕ. ∀v:Point(dM({i})).
((v = 0 ∈ Point(dM({i})))
∨ (v = 1 ∈ Point(dM({i})))
∨ (v = <i> ∈ Point(dM({i})))
∨ (v = <1-i> ∈ Point(dM({i})))
∨ (v = <i> ∧ <1-i> ∈ Point(dM({i})))
∨ (v = <i> ∨ <1-i> ∈ Point(dM({i}))))
Proof
Definitions occuring in Statement :
dM1: 1,
dM0: 0,
dM_opp: <1-x>,
dM_inc: <x>,
dM: dM(I),
lattice-join: a ∨ b,
lattice-meet: a ∧ b,
lattice-point: Point(l),
fset-singleton: {x},
nat: ℕ,
all: ∀x:A. B[x],
or: P ∨ Q,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
top: Top,
subtype_rel: A ⊆r B,
prop: ℙ,
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
rev_implies: P ⇐ Q,
uiff: uiff(P;Q),
uimplies: b supposing a,
dM-deq: dM-deq(I),
free-dml-deq: free-dml-deq(T;eq),
rev_uimplies: rev_uimplies(P;Q),
DeMorgan-algebra: DeMorganAlgebra,
so_lambda: λ2x.t[x],
guard: {T},
so_apply: x[s],
true: True,
squash: ↓T,
nat: ℕ,
names: names(I),
or: P ∨ Q,
deq: EqDecider(T),
dM_opp: <1-x>,
dM_inc: <x>,
dmopp: <1-i>,
dminc: <i>,
free-dl-inc: free-dl-inc(x),
sq_stable: SqStable(P),
not: ¬A,
false: False,
cand: A c∧ B,
decidable: Dec(P),
isl: isl(x),
f-proper-subset: xs ⊆≠ ys,
f-subset: xs ⊆ ys,
deq-fset: deq-fset(eq),
decidable__equal_fset,
decidable_functionality,
iff_preserves_decidability,
decidable__and2,
decidable__f-subset,
decidable__all_fset,
decidable__assert,
fset-null: fset-null(s),
null: null(as),
fset-filter: {x ∈ s | P[x]},
filter: filter(P;l),
reduce: reduce(f;k;as),
list_ind: list_ind,
empty-fset: {},
nil: [],
it: ⋅,
btrue: tt,
decidable__and,
fset-singleton: {x},
cons: [a / b],
ifthenelse: if b then t else f fi ,
bnot: ¬bb,
decidable__fset-member,
deq-fset-member: a ∈b s,
deq-member: x ∈b L,
bfalse: ff,
assert: ↑b,
bool: 𝔹,
fset-pair: {a,b},
bor: p ∨bq,
mk_deq: mk_deq(p),
union-deq: union-deq(A;B;a;b),
sumdeq: sumdeq(a;b),
names-deq: NamesDeq,
int-deq: IntDeq,
eq_int: (i =z j),
iff_weakening_uiff,
fset-all-iff,
fset-add: fset-add(eq;x;s),
fset-union: x ⋃ y,
l-union: as ⋃ bs,
insert: insert(a;L),
eval_list: eval_list(t)
Lemmas referenced :
dM-point,
fset_wf,
names_wf,
fset-singleton_wf,
nat_wf,
assert_wf,
fset-antichain_wf,
union-deq_wf,
names-deq_wf,
equal_wf,
lattice-point_wf,
dM_wf,
assert-deq,
dM-deq_wf,
assert-deq-fset,
deq-fset_wf,
subtype_rel_set,
DeMorgan-algebra-structure_wf,
lattice-structure_wf,
lattice-axioms_wf,
bounded-lattice-structure-subtype,
DeMorgan-algebra-structure-subtype,
subtype_rel_transitivity,
bounded-lattice-structure_wf,
bounded-lattice-axioms_wf,
uall_wf,
lattice-meet_wf,
lattice-join_wf,
DeMorgan-algebra-axioms_wf,
squash_wf,
true_wf,
subtype_rel_self,
iff_weakening_equal,
dM_inc_wf,
member-fset-singleton,
int-deq_wf,
strong-subtype-deq-subtype,
strong-subtype-set3,
le_wf,
strong-subtype-self,
fset-member_wf,
dM_opp_wf,
dM0_wf,
or_wf,
dM1_wf,
decidable__assert,
deq_wf,
all_wf,
decidable_wf,
decidable_functionality,
iff_weakening_uiff,
dM0-sq-empty,
dM1-sq-singleton-empty,
dM-meet-inc-opp,
dM-join-inc-opp,
equal-wf-T-base,
fset-pair_wf,
empty-fset_wf,
sq_stable_from_decidable,
decidable__or,
fset-induction,
sq_stable__all,
equal-wf-base,
equal-wf-base-T,
fset-add_wf,
not_wf,
fset-antichain-add,
fset-extensionality,
and_wf,
fset-member_witness,
uiff_wf,
member_wf,
false_wf,
member-empty-fset,
member-fset-pair,
decidable__fset-member,
btrue_wf,
bfalse_wf,
isl_wf,
btrue_neq_bfalse,
f-proper-subset_wf,
member-fset-add,
it_wf,
subtype_rel_union,
unit_wf2,
f-singleton-subset,
fset-pair-symmetry,
f-subset_wf,
decidable__equal_fset,
iff_preserves_decidability,
decidable__and2,
decidable__f-subset,
decidable__all_fset,
decidable__and,
fset-all-iff
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalRule,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
isect_memberEquality,
voidElimination,
voidEquality,
hypothesis,
lambdaEquality,
setElimination,
rename,
hypothesisEquality,
setEquality,
unionEquality,
independent_pairFormation,
applyEquality,
because_Cache,
productElimination,
independent_isectElimination,
equalityTransitivity,
equalitySymmetry,
instantiate,
productEquality,
cumulativity,
natural_numberEquality,
imageElimination,
universeEquality,
imageMemberEquality,
baseClosed,
independent_functionElimination,
intEquality,
dependent_set_memberEquality,
addLevel,
unionElimination,
inlFormation,
dependent_functionElimination,
inrFormation,
inlEquality,
inrEquality,
functionEquality,
isect_memberFormation,
hyp_replacement,
applyLambdaEquality,
independent_pairEquality,
promote_hyp,
axiomEquality,
int_eqReduceTrueSq
Latex:
\mforall{}i:\mBbbN{}. \mforall{}v:Point(dM(\{i\})).
((v = 0) \mvee{} (v = 1) \mvee{} (v = <i>) \mvee{} (v = ə-i>) \mvee{} (v = <i> \mwedge{} ə-i>) \mvee{} (v = <i> \mvee{} ə-i>))
Date html generated:
2019_11_04-PM-05_31_12
Last ObjectModification:
2018_08_27-PM-01_27_25
Theory : cubical!type!theory
Home
Index