Nuprl Lemma : fl-point

[T:Type]. ∀[eq:EqDecider(T)].
  Point(face-lattice(T;eq)) ≡ {ac:fset(fset(T T))| 
                               (↑fset-antichain(union-deq(T;T;eq;eq);ac))
                               ∧ (∀a:fset(T T). (a ∈ ac  (∀z:T. (inl z ∈ a ∧ inr z  ∈ a)))))} 


Proof




Definitions occuring in Statement :  face-lattice: face-lattice(T;eq) lattice-point: Point(l) fset-antichain: fset-antichain(eq;ac) deq-fset: deq-fset(eq) fset-member: a ∈ s fset: fset(T) union-deq: union-deq(A;B;a;b) deq: EqDecider(T) assert: b ext-eq: A ≡ B uall: [x:A]. B[x] all: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q set: {x:A| B[x]}  inr: inr  inl: inl x union: left right universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T face-lattice: face-lattice(T;eq) top: Top so_lambda: λ2x.t[x] so_apply: x[s] ext-eq: A ≡ B and: P ∧ Q subtype_rel: A ⊆B cand: c∧ B all: x:A. B[x] implies:  Q not: ¬A false: False prop: uiff: uiff(P;Q) uimplies: supposing a face-lattice-constraints: face-lattice-constraints(x) f-subset: xs ⊆ ys or: P ∨ Q squash: T true: True guard: {T} iff: ⇐⇒ Q rev_implies:  Q rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  free-dlwc-point fset-member_wf union-deq_wf fset_wf deq-fset_wf assert_wf fset-antichain_wf all_wf not_wf fset-all_wf fset-contains-none_wf face-lattice-constraints_wf deq_wf fset-all-iff assert-fset-contains-none fset-pair_wf member-fset-singleton fset-member_witness member-fset-pair squash_wf true_wf iff_weakening_equal f-subset_wf assert_witness equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality voidElimination voidEquality hypothesis independent_pairFormation lambdaEquality setElimination rename dependent_set_memberEquality hypothesisEquality productElimination lambdaFormation independent_functionElimination productEquality unionEquality cumulativity inlEquality inrEquality because_Cache functionEquality setEquality independent_pairEquality axiomEquality universeEquality independent_isectElimination dependent_functionElimination equalityTransitivity equalitySymmetry unionElimination applyEquality imageElimination natural_numberEquality imageMemberEquality baseClosed inrFormation hyp_replacement Error :applyLambdaEquality,  inlFormation

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].
    Point(face-lattice(T;eq))  \mequiv{}  \{ac:fset(fset(T  +  T))| 
                                                              (\muparrow{}fset-antichain(union-deq(T;T;eq;eq);ac))
                                                              \mwedge{}  (\mforall{}a:fset(T  +  T).  (a  \mmember{}  ac  {}\mRightarrow{}  (\mforall{}z:T.  (\mneg{}(inl  z  \mmember{}  a  \mwedge{}  inr  z    \mmember{}  a)))))\} 



Date html generated: 2016_10_26-PM-01_01_15
Last ObjectModification: 2016_07_12-AM-09_23_37

Theory : lattices


Home Index