Nuprl Lemma : lattice-join_wf

[l:LatticeStructure]. ∀[a,b:Point(l)].  (a ∨ b ∈ Point(l))


Proof




Definitions occuring in Statement :  lattice-join: a ∨ b lattice-point: Point(l) lattice-structure: LatticeStructure uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T lattice-join: a ∨ b lattice-structure: LatticeStructure record+: record+ record-select: r.x subtype_rel: A ⊆B eq_atom: =a y ifthenelse: if then else fi  btrue: tt lattice-point: Point(l)
Lemmas referenced :  subtype_rel_self lattice-point_wf lattice-structure_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution dependentIntersectionElimination dependentIntersectionEqElimination thin hypothesis applyEquality tokenEquality instantiate lemma_by_obid isectElimination universeEquality functionEquality hypothesisEquality lambdaEquality equalityTransitivity equalitySymmetry axiomEquality isect_memberEquality because_Cache

Latex:
\mforall{}[l:LatticeStructure].  \mforall{}[a,b:Point(l)].    (a  \mvee{}  b  \mmember{}  Point(l))



Date html generated: 2020_05_20-AM-08_23_33
Last ObjectModification: 2015_12_28-PM-02_03_50

Theory : lattices


Home Index