Nuprl Lemma : lattice-meet-idempotent

[l:Lattice]. ∀[u:Point(l)].  (u ∧ u ∈ Point(l))


Proof




Definitions occuring in Statement :  lattice: Lattice lattice-meet: a ∧ b lattice-point: Point(l) uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T lattice: Lattice and: P ∧ Q squash: T prop: true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q
Lemmas referenced :  lattice_properties lattice-point_wf lattice_wf lattice-meet_wf squash_wf true_wf lattice-structure_wf equal_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename productElimination sqequalRule isect_memberEquality axiomEquality because_Cache applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality natural_numberEquality imageMemberEquality baseClosed independent_isectElimination independent_functionElimination hyp_replacement applyLambdaEquality

Latex:
\mforall{}[l:Lattice].  \mforall{}[u:Point(l)].    (u  \mwedge{}  u  =  u)



Date html generated: 2020_05_20-AM-08_25_22
Last ObjectModification: 2017_07_28-AM-09_12_48

Theory : lattices


Home Index