Work at SourceForge, help us to make it a better place! We have an immediate need for a Support Technician in our San Francisco or Denver office.

Close

[4b23aa]: web / entries / LatticeProperties.shtml Maximize Restore History

Download this file

LatticeProperties.shtml    96 lines (78 with data), 3.0 kB

<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
		"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
  <title>Archive of Formal Proofs</title>
  <link rel="stylesheet" type="text/css" href="front.css">
  <link rel="icon" href="../images/favicon.ico" type="image/icon">
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
</head>
<body>

<table width="100%">
  <tbody>
    <tr>
      <td width="20%" align="center" valign="top">
      <!-- navigation -->
      <!--#include file="nav.html"-->
      </td>
      <td width="80%" valign="top">
      <!-- content -->

<div align="center">
<p> </p>

<h1><font class="first">L</font>attice
<font class="first">P</font>roperties
</h1>
<p></p>
<table width="80%" class="data">
  <tbody>
    <tr><td class="datahead" width="20%">Title:</td>
        <td class="data" width="80%">Lattice Properties</td></tr>

    <tr><td class="datahead">Author:</td>
        <td class="data"><a href="http://users.abo.fi/vpreotea/">Viorel Preoteasa</a></td></tr>

    <tr><td class="datahead">Submission date:</td>
        <td class="data">2011-09-22</td></tr>

    <tr><td class="datahead" valign="top">Abstract:</td>
        <td class="abstract">

This formalization introduces and collects some algebraic structures based on lattices and complete lattices for use in other developments. The structures introduced are complete distributive lattices, modular and distributive lattices, as well as lattice ordered groups. In addition to the results proved for the new lattices, this formalization also introduces theorems about latices and distributive lattices in general.
        </td></tr>

    <tr><td class="datahead">License:</td>
        <td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>


<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
<!---INCLUDE- file="devel-warning.shtml"-->

  </tbody>
</table>

<p></p>

<!--#set var="name" value="LatticeProperties" -->
<!--#set var="binfo" value="../browser_info/current/HOL/${name}" -->

<!--#set var="doc" value="${binfo}/document.pdf" -->
<!--#set var="outline" value="${binfo}/outline.pdf" -->
<!--#set var="browse" value="${binfo}/index.html" -->
<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->

<table class="links">
  <tbody>
    <tr>
  <td class="links">
	<a href="<!--#echo var="outline" -->">Proof outline</a><br>
	<a href="<!--#echo var="doc" -->">Proof document</a>
  </td>
	<!-- link to README.hmtl if no document exists -->	
	</tr>
    <tr>
  <td class="links">
	<a href="<!--#echo var="browse" -->">Browse theories</a>
	</td></tr>
    <tr>
  <td class="links"> 
	<a href="<!--#echo var="tar" -->">Download this entry</a>
	</td>
  </tr>
    <tr><td class="links">Older releases:
None    </td></tr>
  </tbody>
</table>
<!-- entry data end -->

</td> </tr> </table>

</body>
</html>