Email Gateway (Aug 18 2022 at 13:56): Email Gateway (Aug 18 2022 at 13:56):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
I am trying to do some theorems about inducing lattice structure on
subsets of partial orders.
I have a theorem, sub_po, that the order relation forms a partial
order when restricted to the subset. I would like resolve sub_po
against various theorems in the partial_order locale, in particular
theorems from parent locales. If I make an interpretation using
sub_po, all these become available, but all my partial_order notation
become ambiguous (copies for parent order and sub-order).
Is there any way to make an interpretation without bringing in the
notation?
Does the mysterious "structure" mechanism have any use here? (Is it
explained anywhere?)
If I don't make an interpretation, how can I get at parent locale
theorems without restating and reproving the parent locale results?
Dr Brendan Mahony
C3I Division ph +61 8 8259 6046
Defence Science and Technology Organisation fx +61 8 8259 5589
Edinburgh, South Australia Brendan.Mahony@dsto.defence.gov.au
Important: This document remains the property of the Australian
Government Department of Defence and is subject to the jurisdiction
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.
IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914. If you have received this email in error, you are requested to contact the sender and delete the email.
Last updated: Nov 21 2024 at 12:39 UTC