Nuprl Lemma : lattice-ble_wf

[l:LatticeStructure]. ∀[eq:EqDecider(Point(l))]. ∀[a,b:Point(l)].  (lattice-ble(l;eq;a;b) ∈ 𝔹)


Proof




Definitions occuring in Statement :  lattice-ble: lattice-ble(l;eq;a;b) lattice-point: Point(l) lattice-structure: LatticeStructure deq: EqDecider(T) bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T lattice-ble: lattice-ble(l;eq;a;b) deq: EqDecider(T)
Lemmas referenced :  lattice-meet_wf lattice-point_wf deq_wf lattice-structure_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule applyEquality sqequalHypSubstitution setElimination thin rename hypothesisEquality lemma_by_obid isectElimination hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[l:LatticeStructure].  \mforall{}[eq:EqDecider(Point(l))].  \mforall{}[a,b:Point(l)].    (lattice-ble(l;eq;a;b)  \mmember{}  \mBbbB{})



Date html generated: 2020_05_20-AM-08_43_06
Last ObjectModification: 2015_12_28-PM-02_01_45

Theory : lattices


Home Index