{"entities":{"Q7361647":{"pageid":31520480,"ns":120,"title":"Item:Q7361647","lastrevid":105367904,"modified":"2026-10-07T13:37:18Z","type":"item","id":"Q7361647","labels":{"en":{"language":"en","value":"Complete Non-Orders and Fixed Points"}},"descriptions":{"en":{"language":"en","value":"AFP entry Complete_Non_Orders"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0d1f163d10511f828f04c20597bd0ab2553505d0","datavalue":{"value":"https://isa-afp.org/entries/Complete_Non_Orders.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361647$C6AA52AD-F10E-4063-BF0C-BF4DBB364671","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"34188037f8b0cd35688ae234ade090010846bddd","datavalue":{"value":{"time":"+2019-06-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361647$1BF8C15F-27B6-4DCA-8BDB-09A83B6A2CCD","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"4e646f16cde9cfa1c19d0771a8f74ba7e8c772f6","datavalue":{"value":"Akihisa Yamada","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361647$D8E52162-F2DE-446B-BCE3-15AB60C5455F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"e5f8bd2643aec22c6a14c3a753e03cb8f232a2bc","datavalue":{"value":"J\u00e9r\u00e9my Dubut","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361647$960D4128-B5FE-4D2A-8581-43A37B0B8324","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ffec7342e81f3a91b915338c6f9fbabb5b79c626","datavalue":{"value":{"text":"Complete Non-Orders and Fixed Points","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361647$2C976374-92E0-41C5-8860-AD16AA66F089","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"82c0baebceb7b6f2e3812f3e9a34a0233b82601e","datavalue":{"value":"We develop an Isabelle/HOL library of order-theoretic concepts, such as various completeness conditions and fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often without any properties of ordering, thus complete non-orders. In particular, we generalize the Knaster\u2013Tarski theorem so that we ensure the existence of a quasi-fixed point of monotone maps over complete non-orders, and show that the set of quasi-fixed points is complete under a mild condition\u2014attractivity\u2014which is implied by either antisymmetry or transitivity. This result generalizes and strengthens a result by Stauti and Maaden. Finally, we recover Kleene\u2019s fixed-point theorem for omega-complete non-orders, again using attractivity to prove that Kleene\u2019s fixed points are least quasi-fixed points.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361647$11B384A2-17A8-4749-BA78-ED236A627D1F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d9190693f3924b86be7203c014f0b8b161bc6f8","datavalue":{"value":{"entity-type":"item","numeric-id":5302559,"id":"Q5302559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$3917AB1B-2F55-40A9-8513-77F60F466474","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1903be4a36187a0a0e197e708bc72f62f93b28bd","datavalue":{"value":{"entity-type":"item","numeric-id":3183520,"id":"Q3183520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$B891C0E3-A82E-4141-918B-AB09AF868F1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7482d7ed8697565cd880232cf548d33b05ae66ec","datavalue":{"value":{"entity-type":"item","numeric-id":743926,"id":"Q743926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$D7C7AB18-A5D2-4DCA-8954-071D76FCCBB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3152b092b3e2fb8c4549523c9224e28afdb3af7","datavalue":{"value":{"entity-type":"item","numeric-id":4898467,"id":"Q4898467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$9850D887-A8D0-4EAE-B9C2-F537DD18D3BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c6891719cea9185328df43316e048fd89a27ee8e","datavalue":{"value":{"entity-type":"item","numeric-id":3366721,"id":"Q3366721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$E4CE61A2-1AFC-4708-B221-B167635C9144","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a3f157eb9fb8ce360dd2db17c88b593e185dced","datavalue":{"value":{"entity-type":"item","numeric-id":2649887,"id":"Q2649887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$F0EFD0A4-2CA7-4032-936E-180EFAF1AF19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b02cebc44c2831878b18e904086383fc947d3037","datavalue":{"value":{"entity-type":"item","numeric-id":5417200,"id":"Q5417200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$C96F7876-536C-440F-AFB9-8D0D5A938F56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ba4f5628b9493b3dc4e9b69bc068cb07ae68c2f","datavalue":{"value":{"entity-type":"item","numeric-id":4530231,"id":"Q4530231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$8F75F390-1A1C-4C6A-B2FC-81DA2C7E4511","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc2f39666e772978fe5e4959c733bcc77f9535be","datavalue":{"value":{"entity-type":"item","numeric-id":5028488,"id":"Q5028488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$0417396B-61DD-40FC-8B65-FB541A36093F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb4857d0d243b746647a153e1690cd4acc84f69e","datavalue":{"value":{"entity-type":"item","numeric-id":5280247,"id":"Q5280247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$20B96988-DC5E-4CA5-80C2-48C21CC51DF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9db762cc0f08fb652d186856f54bfcc71614a4e1","datavalue":{"value":{"entity-type":"item","numeric-id":4787439,"id":"Q4787439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$4E5D47AB-E9CE-429C-AB5F-B1873C955CAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9393b42a89db709a1810e63354bd87bc393c7f4c","datavalue":{"value":{"entity-type":"item","numeric-id":4421936,"id":"Q4421936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$823FD51E-876B-4DE0-8A8C-C0418AC3B928","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"17a69741364102658aa60a87b94db8d7506ce725","datavalue":{"value":{"entity-type":"item","numeric-id":3183517,"id":"Q3183517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$DBE37855-BA35-4E8B-9731-AD483A30A762","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f4334b25d43b9293350a877e2d317280ca55a9","datavalue":{"value":{"entity-type":"item","numeric-id":3543646,"id":"Q3543646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$E80CE4DA-EE8E-4063-B0FF-05695F930A7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$A6392588-8991-436B-B9CB-437F999E925D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07d763717b639e10adfdb52f6d0aed821444ad5f","datavalue":{"value":{"entity-type":"item","numeric-id":2907353,"id":"Q2907353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$44230369-876D-4289-86E4-1C641F83C0D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0aef60bd392ccfb5e82daa98f095917b33d1745","datavalue":{"value":{"entity-type":"item","numeric-id":3183545,"id":"Q3183545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$A14D3F47-8BCB-4CF3-8F7A-F5A5FF018C7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f23d285b53c3197115893f720b8802b1468a917e","datavalue":{"value":{"entity-type":"item","numeric-id":4487279,"id":"Q4487279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$2705EB4F-D55E-49E2-B187-7FB342124732","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ba9fbbe99769fb61e26032cc260cefa2cab3df0","datavalue":{"value":{"entity-type":"item","numeric-id":2723411,"id":"Q2723411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$B558F0C6-D605-4AD2-9D72-D707525A96BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64a266c569519c1799305a98d9e648f4fe04400b","datavalue":{"value":{"entity-type":"item","numeric-id":2646352,"id":"Q2646352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$2C42FFC7-2182-4060-A03D-A3C372B21706","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"49d6115c079e3b52f26b6d7f9e859af953a5bab6","datavalue":{"value":{"entity-type":"item","numeric-id":1051009,"id":"Q1051009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$02897CBA-05A0-4B6C-8DB3-357B6B290599","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9689d3285995afb42633d6587b8f7ef68cfb9e38","datavalue":{"value":{"entity-type":"item","numeric-id":5756774,"id":"Q5756774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$4FA3F2FA-B242-4E53-86C3-8469DBD9938B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cd1db7dcd2da9fc394dcd951ad62461c4f9bd451","datavalue":{"value":{"entity-type":"item","numeric-id":1227632,"id":"Q1227632"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$91ECD4EF-7109-4BA9-AEB6-11B817951249","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"100c7a9e8adba679dbd812d693563f7e95d89f43","datavalue":{"value":{"entity-type":"item","numeric-id":3036268,"id":"Q3036268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$01D25C39-0AA4-4860-A534-2F17C88A112E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"49023bd5aa461c9f63f0725228815aa2af2e478f","datavalue":{"value":{"entity-type":"item","numeric-id":5747646,"id":"Q5747646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$E88CADC4-A5D5-4C1C-BA85-6A8FF2F99967","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbc106b731042db90c61107a1945c225e20e2508","datavalue":{"value":{"entity-type":"item","numeric-id":5287518,"id":"Q5287518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$045C0836-EF79-4F45-8D2E-7A26A069AD5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6b379364cb252742c8efdf365072062c0dfb27c0","datavalue":{"value":{"entity-type":"item","numeric-id":5685626,"id":"Q5685626"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$E4597D60-1DE4-4467-90C2-6FAF2859D71D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c39b9040e3d2807bc13175b6074f0175a0a4a1c","datavalue":{"value":{"entity-type":"item","numeric-id":5747754,"id":"Q5747754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$70E5A0AE-E3A7-4BD0-A7D7-1528CF49D5F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"914d119a8f713d1434d26e4a2c2d1c803ceea4e9","datavalue":{"value":{"entity-type":"item","numeric-id":5410234,"id":"Q5410234"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$A522A61D-104C-4611-98BD-6BC308D60C42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e320d5ab20d9378e83c08a862b63bf2725892d4a","datavalue":{"value":{"entity-type":"item","numeric-id":2653567,"id":"Q2653567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$A97A8FA2-E7AE-43C4-B98A-B4B17142506B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26941f06eb88bf81e38bb13c2d3185e730c6f558","datavalue":{"value":{"entity-type":"item","numeric-id":2553981,"id":"Q2553981"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$0F1B3E17-102B-415C-BBAA-D438F8987C7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de0fc706b8fb2cb22cea7cd4b1a9826b59dd7d2c","datavalue":{"value":{"entity-type":"item","numeric-id":5875442,"id":"Q5875442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$BF9ED3D9-AD84-453B-AF3B-BB7FFA3512EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"232cef772992e51ee75e6d7bfd7d5bead98eb42f","datavalue":{"value":{"entity-type":"item","numeric-id":6643021,"id":"Q6643021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$385A50A8-F9EB-484D-8BDD-B9EF65EA27B9","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$E1BA9E85-090E-4497-AC42-4A44AAB2EF63","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"a4f736a78ec41288f78e3c0d6553d1178e87e9d5","datavalue":{"value":{"entity-type":"item","numeric-id":7360831,"id":"Q7360831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$E1E2DE26-F896-4003-B6DF-ED53CE083B9C","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361647$6E7047B1-FD30-45AE-AF60-1AE60CFCD877","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Complete Non-Orders and Fixed Points","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Complete_Non-Orders_and_Fixed_Points"}}}}}