{"entities":{"Q4910724":{"pageid":6940303,"ns":120,"title":"Item:Q4910724","lastrevid":51673016,"modified":"2026-01-19T09:57:15Z","type":"item","id":"Q4910724","labels":{"en":{"language":"en","value":"Discrete Jordan curve theorem: a proof formalized in Coq with hypermaps"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6146460"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4910724$C4306960-6A8D-49AF-8FF4-16A5ED306EA0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1e5f4595541b11c3cd3ce22bd6eebc33d2acab9c","datavalue":{"value":"1259.68179","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4910724$266CE7F8-A795-4F1D-8BB7-18960A37AA92","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7b9642534f304d9a98032df7352635c1aa31c0f2","datavalue":{"value":{"entity-type":"item","numeric-id":396465,"id":"Q396465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4910724$9EEA369F-627B-4CD7-9EAC-8B917654F4A8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6b36cae3d8cf11c479e6d5b4030a31d81c96c839","datavalue":{"value":{"time":"+2013-03-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4910724$20C497A5-0F2A-4CB3-917B-51CA1BFFF208","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"742d8e865fa429f836685e5ff785b7bee57630db","datavalue":{"value":"http://subs.emis.de/LIPIcs/frontdoor_2fd6.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q4910724$8EA28D1E-D170-4388-9CEA-9699F716FB35","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4910724$A75C9FF5-63DE-44A0-8A78-2EA8E23B6489","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"bd1d0fd44795f1d939549575c09caac8d4530fa6","datavalue":{"value":"54D05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4910724$6D86EC23-D16A-4B18-BE9E-34D2F19A2836","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"003e5de0352cc2bc9f4ac1adce417c8a03d482b4","datavalue":{"value":"6146460","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4910724$2CA62CFC-383C-43A4-94CB-129A6403BAB5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7ac263324871a44dcbba67d80bbe91e299cc16","datavalue":{"value":"formal specifications","type":"string"},"datatype":"string"},"type":"statement","id":"Q4910724$A6EC1C7D-68FE-48D4-B9D9-28E673F673C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5e474a8987a98192748105597575b6fc52489a90","datavalue":{"value":"computational topology","type":"string"},"datatype":"string"},"type":"statement","id":"Q4910724$AF481DA5-7B25-49D2-A2D2-F3BDBB15B1E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83a4003069926cc612c694964e3cbdf707c8f2c7","datavalue":{"value":"computer-aided proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q4910724$B92605C9-6C06-4D15-A858-B1F3EF490AC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q4910724$21B7038E-7F6E-4569-9160-A64E817575C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b98dc2eed6378aa9c9d830839eff64ac891c4bdb","datavalue":{"value":"planar subdivisions","type":"string"},"datatype":"string"},"type":"statement","id":"Q4910724$86D03A50-A860-45A4-9BB5-900D0AA6B57E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8dc5992e44b20c9bb28dceede04bd8419143b6d5","datavalue":{"value":"hypermaps","type":"string"},"datatype":"string"},"type":"statement","id":"Q4910724$5BAC68AE-2530-4472-BD98-17B2F78895A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"47c9c29f3dc602f62b8b8cb46b4cb6f32eeac5cb","datavalue":{"value":"Jordan curve theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q4910724$797D192D-2E4C-4783-A27A-9179D348BBD0","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4910724$EF329D7F-0DB7-4A5D-9E3D-A03855ED3BF0","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4910724$AAEF9A8E-89A6-49C6-BA9B-6489FC6F7B17","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c330c725319c6f72192ebf2cd24abe528d903759","datavalue":{"value":"10.4230/LIPICS.STACS.2008.1349","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4910724$4A9653CB-08B1-41BF-87BF-E6D1F1CC6AC2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"91bc3665e59da0019331d4191b94e7c16de425a3","datavalue":{"value":{"entity-type":"item","numeric-id":839032,"id":"Q839032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e97bebd061596dceaa91e96ee42b2acd8af69bc2","datavalue":{"value":{"amount":"+0.9726371169090272","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4910724$C3FBD700-7959-4B94-89F3-BB2C503DFE06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7b99a9d795cff16b5b9afb195f414bd864e35f2e","datavalue":{"value":{"entity-type":"item","numeric-id":2946657,"id":"Q2946657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9d2abef1d2788eb547b1984d2dd44def9a5e010a","datavalue":{"value":{"amount":"+0.783719003200531","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4910724$8349B60A-0509-4150-8FD9-CA5F057C50B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7775c9516984de3980ea4fc41904d7b81dfe9728","datavalue":{"value":{"entity-type":"item","numeric-id":1882905,"id":"Q1882905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a1472de7bc822be6fdf58aeb23d4a6a0fc2566fe","datavalue":{"value":{"amount":"+0.7721261978149414","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4910724$B708EED2-B32B-4C00-9D5F-DF30C7C7F113","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e34cae745e63b9da78a3adb53a5db76f761f5ae9","datavalue":{"value":{"entity-type":"item","numeric-id":944364,"id":"Q944364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"34b610b672cec99ac6c4234704405cb524b7133c","datavalue":{"value":{"amount":"+0.7633581757545471","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4910724$0CB933A1-D45D-44A3-B975-EE4F38AAE597","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7f1cc5c6b2cc1f60370a57dbce9c9acd8ef47126","datavalue":{"value":{"entity-type":"item","numeric-id":5448058,"id":"Q5448058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4c0d39d1648c98ef2a93bd2fea7e8c1f240ce473","datavalue":{"value":{"amount":"+0.7625995874404907","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4910724$C5D1DAC4-FF3C-4AA3-8167-56E62BA5711F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4910724","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4910724"}}}}}