Nuprl Lemma : implies-le-face-lattice-join

T:Type. ∀eq:EqDecider(T). ∀x,y,z:Point(face-lattice(T;eq)).
  ((∀s:fset(T T). (s ∈  ((↓∃t:fset(T T). (t ∈ x ∧ t ⊆ s)) ∨ (↓∃t:fset(T T). (t ∈ y ∧ t ⊆ s)))))  z ≤ x ∨ y)


Proof




Definitions occuring in Statement :  face-lattice: face-lattice(T;eq) lattice-le: a ≤ b lattice-join: a ∨ b lattice-point: Point(l) deq-fset: deq-fset(eq) f-subset: xs ⊆ ys fset-member: a ∈ s fset: fset(T) union-deq: union-deq(A;B;a;b) deq: EqDecider(T) all: x:A. B[x] exists: x:A. B[x] squash: T implies:  Q or: P ∨ Q and: P ∧ Q union: left right universe: Type
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T top: Top subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] and: P ∧ Q prop: implies:  Q iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) uimplies: supposing a squash: T exists: x:A. B[x] or: P ∨ Q bdd-distributive-lattice: BoundedDistributiveLattice face-lattice: face-lattice(T;eq) fset-constrained-ac-lub: lub(P;ac1;ac2) cand: c∧ B
Lemmas referenced :  subtype_rel_sets fset-ac-lub-covers free-dlwc-join deq_wf lattice-meet_wf equal_wf uall_wf bounded-lattice-axioms_wf bounded-lattice-structure-subtype lattice-axioms_wf lattice-structure_wf bounded-lattice-structure_wf subtype_rel_set lattice-point_wf f-subset_wf exists_wf squash_wf or_wf all_wf deq-fset_wf fset-member_wf ac-covers_wf assert-ac-covers face-lattice_wf lattice-join_wf face-lattice-le face-lattice-constraints_wf fset-contains-none_wf fset-all_wf union-deq_wf fset-antichain_wf assert_wf and_wf fset_wf fl-point-sq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality voidElimination voidEquality hypothesis lambdaEquality setElimination rename hypothesisEquality setEquality unionEquality dependent_functionElimination applyEquality because_Cache productElimination independent_functionElimination introduction independent_pairFormation independent_isectElimination addLevel allFunctionality impliesFunctionality orFunctionality levelHypothesis promote_hyp allLevelFunctionality impliesLevelFunctionality orLevelFunctionality imageElimination imageMemberEquality baseClosed cumulativity functionEquality productEquality instantiate universeEquality

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}x,y,z:Point(face-lattice(T;eq)).
    ((\mforall{}s:fset(T  +  T)
            (s  \mmember{}  z  {}\mRightarrow{}  ((\mdownarrow{}\mexists{}t:fset(T  +  T).  (t  \mmember{}  x  \mwedge{}  t  \msubseteq{}  s))  \mvee{}  (\mdownarrow{}\mexists{}t:fset(T  +  T).  (t  \mmember{}  y  \mwedge{}  t  \msubseteq{}  s)))))
    {}\mRightarrow{}  z  \mleq{}  x  \mvee{}  y)



Date html generated: 2020_05_20-AM-08_52_39
Last ObjectModification: 2016_01_20-PM-10_31_03

Theory : lattices


Home Index