Nuprl Lemma : fl-meet-0-1
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ((x=0) ∧ (x=1) = 0 ∈ Point(face-lattice(T;eq)))
Proof
Definitions occuring in Statement :
face-lattice1: (x=1),
face-lattice0: (x=0),
face-lattice: face-lattice(T;eq),
lattice-0: 0,
lattice-meet: a ∧ b,
lattice-point: Point(l),
deq: EqDecider(T),
uall: ∀[x:A]. B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
guard: {T},
prop: ℙ,
or: P ∨ Q,
uimplies: b supposing a,
and: P ∧ Q,
uiff: uiff(P;Q),
implies: P ⇒ Q,
face-lattice-constraints: face-lattice-constraints(x),
all: ∀x:A. B[x],
so_lambda: λ2x.t[x],
so_apply: x[s],
face-lattice: face-lattice(T;eq),
fset-pair: {a,b},
fset-image: f"(s),
f-union: f-union(domeq;rngeq;s;x.g[x]),
top: Top,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
empty-fset: {},
fl-deq: fl-deq(T;eq),
subtype_rel: A ⊆r B,
bdd-distributive-lattice: BoundedDistributiveLattice,
true: True,
squash: ↓T,
iff: P ⇐⇒ Q,
lattice-fset-meet: /\(s),
rev_implies: P ⇐ Q
Lemmas referenced :
deq_wf,
istype-universe,
fset-singleton_wf,
fset_wf,
fset-member_wf,
equal_wf,
member-fset-pair,
fset-pair_wf,
union-deq_wf,
deq-fset_wf,
member-fset-singleton,
free-dlwc-satisfies-constraints,
face-lattice-constraints_wf,
list_accum_cons_lemma,
istype-void,
list_accum_nil_lemma,
face-lattice0-is-inc,
face-lattice1-is-inc,
face-lattice0_wf,
face-lattice1_wf,
fl-deq_wf,
face-lattice_wf,
lattice-fset-meet_wf,
bdd-distributive-lattice-subtype-bdd-lattice,
decidable-equal-deq,
lattice-point_wf,
subtype_rel_set,
bounded-lattice-structure_wf,
lattice-structure_wf,
uall_wf,
bounded-lattice-structure-subtype,
fset-union_wf,
lattice-axioms_wf,
bounded-lattice-axioms_wf,
lattice-meet_wf,
lattice-join_wf,
empty-fset_wf,
lattice-0_wf,
squash_wf,
true_wf,
lattice-fset-meet-union,
lattice-fset-meet-singleton,
subtype_rel_self,
iff_weakening_equal,
reduce_nil_lemma,
lattice-1-meet
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
hypothesis,
universeIsType,
hypothesisEquality,
sqequalRule,
sqequalHypSubstitution,
isect_memberEquality_alt,
isectElimination,
thin,
axiomEquality,
isectIsTypeImplies,
inhabitedIsType,
extract_by_obid,
instantiate,
universeEquality,
inrFormation,
applyLambdaEquality,
hyp_replacement,
inlFormation,
equalitySymmetry,
equalityTransitivity,
dependent_functionElimination,
independent_isectElimination,
productElimination,
unionEquality,
because_Cache,
inrEquality,
cumulativity,
inlEquality,
rename,
unionElimination,
lambdaFormation,
lambdaEquality_alt,
unionIsType,
independent_functionElimination,
inlEquality_alt,
inrEquality_alt,
voidElimination,
lambdaFormation_alt,
equalityIsType1,
applyEquality,
productEquality,
setElimination,
natural_numberEquality,
imageElimination,
imageMemberEquality,
baseClosed
Latex:
\mforall{}[T:Type]. \mforall{}[eq:EqDecider(T)]. \mforall{}[x:T]. ((x=0) \mwedge{} (x=1) = 0)
Date html generated:
2020_05_20-AM-08_51_33
Last ObjectModification:
2018_11_08-PM-06_00_35
Theory : lattices
Home
Index