Nuprl Lemma : lattice-fset-meet-is-glb

[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))].
  ((∀[s:fset(Point(l))]. ∀[x:Point(l)].  /\(s) ≤ supposing x ∈ s)
  ∧ (∀[s:fset(Point(l))]. ∀[v:Point(l)].  ((∀x:Point(l). (x ∈  v ≤ x))  v ≤ /\(s))))


Proof




Definitions occuring in Statement :  lattice-fset-meet: /\(s) bdd-lattice: BoundedLattice lattice-le: a ≤ b lattice-point: Point(l) fset-member: a ∈ s fset: fset(T) deq: EqDecider(T) uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] implies:  Q and: P ∧ Q
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q all: x:A. B[x] uimplies: supposing a lattice-le: a ≤ b prop: implies:  Q so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B bdd-lattice: BoundedLattice sq_stable: SqStable(P) top: Top false: False guard: {T} fset-add: fset-add(eq;x;s) squash: T true: True iff: ⇐⇒ Q rev_implies:  Q or: P ∨ Q empty-fset: {} lattice-fset-meet: /\(s) greatest-lower-bound: greatest-lower-bound(T;x,y.R[x; y];a;b;c)
Lemmas referenced :  fset_wf all_wf fset-member_wf lattice-le_wf deq_wf lattice-point_wf subtype_rel_set bounded-lattice-structure_wf lattice-structure_wf lattice-axioms_wf bounded-lattice-axioms_wf bounded-lattice-structure-subtype bdd-lattice_wf fset-induction uall_wf isect_wf lattice-fset-meet_wf decidable-equal-deq sq_stable__uall squash_wf mem_empty_lemma empty-fset_wf fset-add_wf not_wf sq_stable__equal lattice-meet_wf true_wf lattice-fset-meet-union fset-singleton_wf iff_weakening_equal lattice-fset-meet-singleton member-fset-add lattice-le_transitivity bdd-lattice-subtype-lattice lattice-meet-le lattice-le_weakening sq_stable__all reduce_nil_lemma le-lattice-1 lattice-meet-is-glb equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation thin sqequalHypSubstitution dependent_functionElimination hypothesisEquality hypothesis sqequalRule isect_memberEquality isectElimination axiomEquality because_Cache equalityTransitivity equalitySymmetry extract_by_obid lambdaEquality functionEquality productElimination independent_pairEquality applyEquality instantiate productEquality cumulativity independent_isectElimination independent_functionElimination lambdaFormation voidElimination voidEquality imageElimination natural_numberEquality imageMemberEquality baseClosed unionElimination hyp_replacement applyLambdaEquality inlFormation inrFormation

Latex:
\mforall{}[l:BoundedLattice].  \mforall{}[eq:EqDecider(Point(l))].
    ((\mforall{}[s:fset(Point(l))].  \mforall{}[x:Point(l)].    /\mbackslash{}(s)  \mleq{}  x  supposing  x  \mmember{}  s)
    \mwedge{}  (\mforall{}[s:fset(Point(l))].  \mforall{}[v:Point(l)].    ((\mforall{}x:Point(l).  (x  \mmember{}  s  {}\mRightarrow{}  v  \mleq{}  x))  {}\mRightarrow{}  v  \mleq{}  /\mbackslash{}(s))))



Date html generated: 2020_05_20-AM-08_44_11
Last ObjectModification: 2017_07_28-AM-09_14_04

Theory : lattices


Home Index