### 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 ⊆r B` eq_atom: `x =a y` ifthenelse: `if b then t else f 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: 2016_05_18-AM-11_19_24
Last ObjectModification: 2015_12_28-PM-02_03_50

Theory : lattices

Home Index