Porządki dobrze ufundowane

Zadanie ma na celu dowiedzenie pewnych własności rozszerzenia leksykograficznego danej relacji. Ewentualną kontynuacją byłoby zdefiniowanie rozszerzenia multizbiorowego i dowiedzenie dla niego podobnych własności.

Używane będzie pojęcie "`pięknej relacji'', zdefiniowane następująco:
Relacja ltA Î A× A jest piękna, jeśli z każdego nieskończonego ciągu {ai}i Î N można wybrać pare indeksów i<j t.że (ltA  ai  aj) lub ai=aj.
Alternatywna (równoważna) własność definiująca piękność relacji to:
z każdego nieskończonego ciągu {ai}i Î N można wybrać podciąg {aij}j Î N t.że dla każdego j zachodzi (ltA  aij  aij+1) lub aij=aij+1.
Państwa zadaniem będzie:
  1. obejrzenie i zrozumienie definicji rozszerzenia leksykograficznego danej relacji ltA na zbiorze A na listy elementów z A (Definicja Ltl jest w pliku theories/Relations/Relation_Operators.v i używa leA jako nazwy rozszerzanej relacji. Jednak nazwa ltA wydaje się sensowniejsza.1)
  2. zdefiniowanie Ltlen -- ograniczenia Ltl do list o równej długości
  3. dowiedzenie, że jeśli ltA jest dobrze ufundowane (definicja well_founded w pliku theories/Init/Wf.v), to Ltlen też jest dobrze ufundowane
  4. zdefiniowanie pojęcia ``bycia ostrym porządkiem'' (chodzi o zdefiniowanie własności, które ostry porządek musi spełniać -- w stylu definicji z pliku theories/Relations/Relation_Definitions.v)
  5. dowiedzenie, że jeśli ltA jest ostrym porządkiem, to Ltl i Ltlen też są ostrymi porządkami
  6. zdefiniowanie pięknej relacji
  7. dowiedzenie, że każde rozszerzenie (w sensie zawierania relacji) pięknej relacji jest piękną relacją
  8. dowiedzenie, że rozszerzenie leksykograficzne z ograniczoną długością Ltlen pięknej relacji jest piękną relacją
  9. (*)dowiedzenie, że każda piękna relacja jest dobrze ufundowana



Jacek Chrząszcz, 11 kwietnia 2002 ostatnia zmiana: May 23, 2002
1
le -- ``less or equal'', lt -- ``less than'' -- rozszerzanie leksykograficzne relacji ``nieostrej'' nie wydaje się być sensowne

This document was translated from LATEX by HEVEA.