[Mnshs.perms.paris] [Perms.paris] [Perms] [Permanents] [Current] Séminaire AA : Jérémy Dubut, Fixed-Point Theorems for Non-Transitive Relations, aujourd'hui 15h, KB204

Bonjour, Le prochain séminaire de l'équipe Automates & Applications aura lieu aujourd'hui à 15h, en mode hybride (KB204 en présentiel). L'orateur sera Jérémy Dubut, les détails de son talk sont à retrouver ci-dessous : * Monday 26 February, 15:00 at EPITA KB 204<https://epimap.fr/kb/voltaire/2> and online (link at https://www.lre.epita.fr/automata_seminars/ when available) * Speaker: Jérémy Dubut-Kross<https://jeremydubut.com/>m/>, National Institute of Advanced Science and Technology, Tokyo * Title: Fixed-Point Theorems for Non-Transitive Relations * We develop an Isabelle/HOL library of order-theoretic fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often with only antisymmetry or attractivity, a mild condition implied by either antisymmetry or transitivity. In particular, we generalize various theorems ensuring the existence of a quasi-fixed point of monotone maps over complete relations, and show that the set of (quasi-)fixed points is itself complete. This result generalizes and strengthens theorems of Knaster-Tarski, Bourbaki-Witt, Kleene, Markowsky, Pataraia, Mashburn, Bhatta-George, and Stouti-Maaden. Joint work with Akihisa Yamada. Bonne journée, -- Daniel STAN ______________________ Current mailing list -- current(a)ml.lre.epita.fr https://lists.lrde.epita.fr/postorius/lists/current.ml.lre.epita.fr// ______________________ Permanents mailing list -- permanents(a)ml.lre.epita.fr https://lists.lrde.epita.fr/postorius/lists/permanents.ml.lre.epita.fr// ______________________ Perms mailing list -- perms(a)ml.lre.epita.fr https://lists.lrde.epita.fr/postorius/lists/perms.ml.lre.epita.fr// ______________________ Perms.paris mailing list -- perms.paris(a)ml.lre.epita.fr https://lists.lrde.epita.fr/postorius/lists/perms.paris.ml.lre.epita.fr//