Nuprl Lemma : lattice-join-0

[l:BoundedLattice]. ∀[x:Point(l)].  ((0 ∨ x ∈ Point(l)) ∧ (x ∨ x ∈ Point(l)))


Proof




Definitions occuring in Statement :  bdd-lattice: BoundedLattice lattice-0: 0 lattice-join: a ∨ b lattice-point: Point(l) uall: [x:A]. B[x] and: P ∧ Q equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q cand: c∧ B bdd-lattice: BoundedLattice subtype_rel: A ⊆B so_lambda: λ2x.t[x] prop: so_apply: x[s] uimplies: supposing a guard: {T} lattice-axioms: lattice-axioms(l) squash: T true: True iff: ⇐⇒ Q rev_implies:  Q implies:  Q bounded-lattice-axioms: bounded-lattice-axioms(l)
Lemmas referenced :  lattice-point_wf subtype_rel_set bounded-lattice-structure_wf lattice-structure_wf lattice-axioms_wf bounded-lattice-structure-subtype bounded-lattice-axioms_wf bdd-lattice_wf lattice-0_wf and_wf equal_wf squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename productElimination hypothesis independent_pairFormation sqequalRule independent_pairEquality axiomEquality extract_by_obid isectElimination hypothesisEquality applyEquality instantiate lambdaEquality productEquality cumulativity independent_isectElimination isect_memberEquality because_Cache hyp_replacement equalitySymmetry dependent_set_memberEquality equalityTransitivity applyLambdaEquality imageElimination universeEquality natural_numberEquality imageMemberEquality baseClosed independent_functionElimination

Latex:
\mforall{}[l:BoundedLattice].  \mforall{}[x:Point(l)].    ((0  \mvee{}  x  =  x)  \mwedge{}  (x  \mvee{}  0  =  x))



Date html generated: 2017_10_05-AM-00_31_21
Last ObjectModification: 2017_07_28-AM-09_13_03

Theory : lattices


Home Index