{"entities":{"Q682381":{"pageid":684230,"ns":120,"title":"Item:Q682381","lastrevid":63775071,"modified":"2026-04-11T15:27:54Z","type":"item","id":"Q682381","labels":{"en":{"language":"en","value":"A formalization of metric spaces in HOL Light"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6833781"}},"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":"Q682381$BCBBC932-F98A-4BE1-B35D-D310582C0174","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2ee74c9257c8fd8ef145936b2d708bb84868f984","datavalue":{"value":{"text":"A formalization of metric spaces in HOL Light","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q682381$8197CF1C-99A8-450A-9844-0AB46AF85AB0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"92ecc4f877710fe4a22da95c8fc6c01b6b576c9a","datavalue":{"value":"1425.68376","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q682381$E78757FD-EEC4-4BF2-98C4-E81E4DF18ABE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ea229d5c7d566db264a7e69175c2b14cf582fccb","datavalue":{"value":{"entity-type":"item","numeric-id":438545,"id":"Q438545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682381$85414D15-186C-47B8-A345-10F554720EE8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682381$64C3C610-3228-46C6-8C10-75F727ACD3D9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3340cc79e75714646430612898cfc312969e0dd0","datavalue":{"value":{"time":"+2018-02-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q682381$C80521E4-C666-4E3D-8287-7BFD40B57E3E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q682381$12EF341E-3E17-408E-9563-56F2FCA7BF5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9934057d10323980704e6b94db4ebac54a6fd5ff","datavalue":{"value":"54E35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q682381$E491FDF2-3913-4DD8-BA9F-D2D7E17A9B61","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ca453fefb6ea05bb64077142f807aed60a3fb141","datavalue":{"value":"6833781","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q682381$B24A1279-028C-43C5-A6B6-06D423E6FBFF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"658126897c7f6bf3db78fea48b2876524c1d8c9e","datavalue":{"value":"formalization of mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q682381$313FBAEB-2885-4E8A-8621-36A50560D092","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q682381$CFEF1ABC-8F43-44F3-A110-00A6A79C1C27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"880958f8426d35e1b206252f9c79a8da7b632921","datavalue":{"value":"metric spaces","type":"string"},"datatype":"string"},"type":"statement","id":"Q682381$F85AA3EC-B94C-4811-B562-B3CBD14FAD5C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682381$EBB73BC8-59EF-477A-A1D2-76F6DCF63D7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682381$07284C68-5B0D-4808-A7A2-F30FD7635872","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b799da0cc0efb29a46dd283874e64386ca0e87dd","datavalue":{"value":{"entity-type":"item","numeric-id":21136,"id":"Q21136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682381$30D4D794-A725-4665-926F-7066D6766067","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":"Q682381$FA08F7BF-B918-40EC-9D4D-E4EAD5BE2514","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"03ec3b537b6a7247661ff77f4f0c10e1487217da","datavalue":{"value":"https://doi.org/10.1007/s10817-017-9412-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q682381$ECC1CEF5-29BD-4A10-84C5-9DADA27C83EB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7ba59fdecb7067bae2cd671cf35c0a3c263a2ef6","datavalue":{"value":"W2289810656","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q682381$920E3087-1E95-49A3-8BA2-644510764413","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a5e182d22cd63374751049cb1ad374f0b5175f7","datavalue":{"value":{"entity-type":"item","numeric-id":5477650,"id":"Q5477650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682381$F5428744-AC1C-44E2-988A-D2F22CAA12BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9055b0cc60b35ae226978f59203587ec6cf2e814","datavalue":{"value":{"entity-type":"item","numeric-id":714712,"id":"Q714712"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682381$CA5A4C20-1053-4735-9EA9-4A313533CEF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa946e46dd7fe5ebbecad5b92f77605dd2ee5cd0","datavalue":{"value":{"entity-type":"item","numeric-id":1319391,"id":"Q1319391"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682381$FE36B05F-8484-466F-B462-04C1BC0E1A18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b6f4b63bc26052368e7b5944153c26fe1fa531","datavalue":{"value":{"entity-type":"item","numeric-id":2914756,"id":"Q2914756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682381$8E4089D5-37E2-4B85-9911-47FDEC8AD7A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3790971f84a7b972ee9e0231ff1aa7d72170d32c","datavalue":{"value":{"entity-type":"item","numeric-id":5327365,"id":"Q5327365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682381$73973914-026A-428A-BDB4-D5697CD4DBEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69c6053474c8a47b1b2379bcf1ce5d891da3ba61","datavalue":{"value":{"entity-type":"item","numeric-id":5848416,"id":"Q5848416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682381$38927294-47FF-48B5-9234-E22E4BF108D4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d51cfe9ba906e06187ccb7b1efc31b86cf445b87","datavalue":{"value":"10.1007/S10817-017-9412-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q682381$B8D5E944-6136-4A00-BDD0-585A64ACA21A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5917cef10283768771f78eab4f40635731cd570e","datavalue":{"value":{"entity-type":"item","numeric-id":1945903,"id":"Q1945903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"89e3cbac0f6c8fdf9a13731428feeaf8a023b48e","datavalue":{"value":{"amount":"+0.790221095085144","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":"Q682381$798893FE-E69B-44F8-942F-B60995E6D0C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"030a8e9ac6fc09570217d40508a4a4eabc57af6f","datavalue":{"value":{"entity-type":"item","numeric-id":5477650,"id":"Q5477650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0310f76cc1559243db551a5f12172937b8af3dc1","datavalue":{"value":{"amount":"+0.7872986793518066","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":"Q682381$70F2500F-A122-4A4C-9BB9-C595E238DB95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b0ef3e16688368de9df60086640e09b844c8b306","datavalue":{"value":{"entity-type":"item","numeric-id":5302828,"id":"Q5302828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"61bcf26ba291f82d0b6e1b682eeabc261aa42379","datavalue":{"value":{"amount":"+0.738007128238678","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":"Q682381$FF03EFD6-BBB5-4B43-BF8D-0A826386A173","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18af68409172bb01e965f879199493ab0097ef10","datavalue":{"value":{"entity-type":"item","numeric-id":516741,"id":"Q516741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8fe38668e23c3fecde13a352a2906480b26a1db7","datavalue":{"value":{"amount":"+0.709122896194458","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":"Q682381$84F128C1-FFB0-42D5-A974-3251B17992F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"70308abe7ca916902344168478639eb5d40daba0","datavalue":{"value":{"entity-type":"item","numeric-id":3107101,"id":"Q3107101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e9c0e99f7267b5031027013f495e1e1305cc7d25","datavalue":{"value":{"amount":"+0.7070838212966919","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":"Q682381$6F51FB1A-B947-4CED-A39B-6071DBE85BF2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A formalization of metric spaces in HOL Light","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_formalization_of_metric_spaces_in_HOL_Light"}}}}}