{"entities":{"Q4504968":{"pageid":6534561,"ns":120,"title":"Item:Q4504968","lastrevid":89508866,"modified":"2026-06-04T17:32:58Z","type":"item","id":"Q4504968","labels":{"en":{"language":"en","value":"Mechanizing Nonstandard Real Analysis"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1509489"}},"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":"Q4504968$DE9CDB7A-7B0C-4889-BD59-C813C46E6715","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b3212f11f2fdb69237179f2e8d288daec665a5eb","datavalue":{"value":{"text":"Mechanizing Nonstandard Real Analysis","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4504968$429E3331-DFCB-44AE-AEAE-F6E3228467E4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"074b6cecf3bfd51355bab2ff47b919f1325ede61","datavalue":{"value":"0951.03006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4504968$06F19F37-94AF-4323-8D08-BAC1882FC16B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"89d55ec5240ba3241d8640dc221bc3935755f633","datavalue":{"value":"10.1112/S1461157000000267","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4504968$17053F75-5E44-48FC-96AA-77B373F11785","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"997f8e81aafe849f90a25017f3ed07a2b1feb16c","datavalue":{"value":{"entity-type":"item","numeric-id":2709391,"id":"Q2709391"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$B7617E9C-5AE2-4C16-B7EB-EB6C548D0B72","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a0d7008e8447ba410a216087c18a25ea2beb179d","datavalue":{"value":{"time":"+2000-09-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4504968$77BBD1D0-4C43-4AD1-859E-1C2B021C7226","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d56aded0c5ed5561827a5198e0e3b1b8a8282d2c","datavalue":{"value":"http://www.lms.ac.uk/jcm/3/lms1999-027/","type":"string"},"datatype":"url"},"type":"statement","id":"Q4504968$24C832A8-6CD9-42CE-B2F1-95D5DD4789FF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4504968$F598DB11-C33C-499F-883A-7B6DF3B0239F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6db4aec5ef7fbf0e828c6d2589c9166d8caea5c3","datavalue":{"value":"03H05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4504968$B24DAE88-58F1-4752-A33C-68B0490D8A1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"df8574ca221627a3b631e5712574287946b0b18d","datavalue":{"value":"26E35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4504968$94CF2DF7-4617-47C6-863A-3A11D7E4D785","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4504968$90E0D72A-F153-4E5F-A8C7-D7DA6101C1BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4504968$67AA618E-949F-4EA9-A89B-F2E17B61F97A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ac3542c07197a97d6633581cda546df5abbf3dc2","datavalue":{"value":"1509489","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4504968$19EAA0D9-EF87-48D8-8FB2-512BAEA60DB4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"99ee3855cbb7b6944214dba708a0269142897d72","datavalue":{"value":"hyperreals","type":"string"},"datatype":"string"},"type":"statement","id":"Q4504968$FE8F60D5-3469-408C-9E16-0F934AF233AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0ed771d6b1c385b1658d733468661da72990db2e","datavalue":{"value":"theorem-prover Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q4504968$47D5C681-F6A2-45B2-BFD0-91E33B35A1F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4504968$71D282BF-9D01-4447-A53A-AB528ADE6FA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb481aa62ce75b6f03de45122f265ebabcb5ae94","datavalue":{"value":"infinitesimals","type":"string"},"datatype":"string"},"type":"statement","id":"Q4504968$293FF967-E8AF-4216-BF9D-7AEB70A7144B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b73cf27f6b1ec0d963b927237b3b12c7759e755c","datavalue":{"value":"infinite numbers","type":"string"},"datatype":"string"},"type":"statement","id":"Q4504968$E265E0BF-3A9F-4D95-90D4-4EC8F8829E46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a11cf132947b7b29693c82a290ecbf2e4989b042","datavalue":{"value":"nonstandard analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q4504968$CB3EC4EC-88C6-48D2-A7B1-79E6F87146A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2fde32cd68a42e4449475681b170c87e0976d509","datavalue":{"value":"filters","type":"string"},"datatype":"string"},"type":"statement","id":"Q4504968$18B20AEC-8AC8-4557-BA8B-458684471192","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9256724b8e750d74d5ea25645b17fc8bb369e885","datavalue":{"value":"ultrafilters","type":"string"},"datatype":"string"},"type":"statement","id":"Q4504968$F13D4839-B83B-4657-912C-92E71DC261F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"950087fd452988354899d8a21e17364c7892e79f","datavalue":{"value":"mechanical theorem-proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q4504968$DEE18871-BE41-43BE-8F96-1FEB54385D6A","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"f08a94e03916a32af2ba279352d8ffef8fc0122f","datavalue":{"value":"Q57382694","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4504968$6242BDBD-EA40-45EF-8A9D-BDF38207B8E3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8d78e8b1fd2bada0896418639974db329feb4fe3","datavalue":{"value":{"entity-type":"item","numeric-id":2102945,"id":"Q2102945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$2AD2634E-6B57-4DD9-A4D8-0A330F635BF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$18874E41-44C8-463C-B589-EF03494C943B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$84A7AFD0-7C3F-4A6D-B5CD-BABCC6733019","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":"Q4504968$7C704120-89D8-4330-B006-A6B5459E93E2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f68752e4f4ac73a30b6079d25b0713ba140693c0","datavalue":{"value":{"entity-type":"item","numeric-id":1099149,"id":"Q1099149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$614DE769-E687-4BB4-A5A7-D4F3AE627E5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca7e027091589776f78a6d7ad8457e805c17b28","datavalue":{"value":{"entity-type":"item","numeric-id":5777498,"id":"Q5777498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$04EA2461-9798-4951-90AC-115AC136DF98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c68052ce980dd5c73b389c61f7735005cb694e59","datavalue":{"value":{"entity-type":"item","numeric-id":4836046,"id":"Q4836046"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$33FA2361-30CA-4E86-9598-B59005739CD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5fc744c8c748de53e360cde6b1b8bb036c2c849","datavalue":{"value":{"entity-type":"item","numeric-id":4853341,"id":"Q4853341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$D7B29D53-5529-45EE-9E69-93B4019C0A47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce52b549975f2f1eb2794b7e93bf906aadaa4ff7","datavalue":{"value":{"entity-type":"item","numeric-id":4131708,"id":"Q4131708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$24DB512D-0A07-446F-967B-53FDF3B5006F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2fdda5ebb9b15dda1ccb4232e3fae8013f458c17","datavalue":{"value":{"entity-type":"item","numeric-id":4104164,"id":"Q4104164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$D0F11F4C-43B8-4F4B-87B1-6A3704709A2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b810f4d936d56c6c13ac6603fda4040c5361d21b","datavalue":{"value":{"entity-type":"item","numeric-id":4353856,"id":"Q4353856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$EF7394F9-97CA-43A5-88C2-066E9A85003C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea2a8fb219c6e1b452da4165b50d68a0ef9a2bdc","datavalue":{"value":{"entity-type":"item","numeric-id":3708229,"id":"Q3708229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$5D6094D0-EFEC-4AE7-8989-87971F3347C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6496304f13783e82d12a275120aa4626825ea47b","datavalue":{"value":{"entity-type":"item","numeric-id":4231030,"id":"Q4231030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$2770338A-99B6-497F-9C18-38DDF83C06BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$7F422111-19E5-4030-892B-620CD27E71D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df566ef0248fe3e927a10046fdd99e599cbaa541","datavalue":{"value":{"entity-type":"item","numeric-id":5961491,"id":"Q5961491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$39A91A58-E6F3-4F9D-807E-EEDB98AF175F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$88C9D57B-4C04-4977-A0E3-14787D9A2788","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ab3bdd7d7fbfac1006a4b16e8a3687950389993","datavalue":{"value":{"entity-type":"item","numeric-id":4099541,"id":"Q4099541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4504968$2F64C2AA-1FD4-4910-BA8C-4B6643A508B2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1f339e081a10eda27036b86ce6f9f0a10ba98ccc","datavalue":{"value":"W1981484178","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4504968$1D8A8B67-07D6-4E7A-ABA5-69FB92F25BDC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a8bfe1579abd1aa529055d84308768a923e2bf5d","datavalue":{"value":{"entity-type":"item","numeric-id":2754041,"id":"Q2754041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fabcabb7c5fae5483d731d944ec0efe41b7ff238","datavalue":{"value":{"amount":"+0.8424417972564697","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":"Q4504968$3A78B026-2BC3-48B1-BE92-0FFC328567CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"52785f2dd2003261c737010c9dd8c0d12eaa464a","datavalue":{"value":{"entity-type":"item","numeric-id":1334896,"id":"Q1334896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c72c5e2dcde782ee5723c73f7b7d70e6fabe9c36","datavalue":{"value":{"amount":"+0.7844447493553162","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":"Q4504968$593379E3-5909-427F-B84A-E3182CE74CFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"28b64cc58f0e3cd3ce8d83be3d83805aa62c9120","datavalue":{"value":{"entity-type":"item","numeric-id":2739733,"id":"Q2739733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3a67c0a5ffd0ac4a6f378225d5fa381551062b4c","datavalue":{"value":{"amount":"+0.7818871736526489","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":"Q4504968$069A0A9E-930A-4BDC-85DA-4B3E5CCB5867","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"babbd8aef74a614f7b4a3930c820eb43cf468863","datavalue":{"value":{"entity-type":"item","numeric-id":1892939,"id":"Q1892939"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2009038cb41422477c3a9b57bdf2d539594f8d1a","datavalue":{"value":{"amount":"+0.778010368347168","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":"Q4504968$A77CFE4D-A96F-4EDB-B754-483D084ADFBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0c5829d3ffd69a9060388ba2482bcabc1c2a84e1","datavalue":{"value":{"entity-type":"item","numeric-id":2720298,"id":"Q2720298"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7d51a1da095da278de53e7c75e7b1d1e8018382","datavalue":{"value":{"amount":"+0.7753512859344482","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":"Q4504968$561B93A1-EBDF-4845-88FC-AFC83F26D7E3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mechanizing Nonstandard Real Analysis","badges":[]}}}}}