{"entities":{"Q6174524":{"pageid":13309412,"ns":120,"title":"Item:Q6174524","lastrevid":55476109,"modified":"2026-02-17T17:17:06Z","type":"item","id":"Q6174524","labels":{"en":{"language":"en","value":"A Coq formalization of Lebesgue induction principle and Tonelli's theorem"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7728835"}},"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":"Q6174524$5903E17D-3D2A-425B-90AD-6AA36054870C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3714affc3e1deebd2a15f0874355f2e40ab53495","datavalue":{"value":{"text":"A Coq formalization of Lebesgue induction principle and Tonelli's theorem","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6174524$8424AFF4-205F-4ED8-8DBE-335687D35083","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e8c235a219197dac85ec341d5ca4db969ce3c1a4","datavalue":{"value":"1529.68315","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6174524$BD5B0DA1-5E4E-4777-B576-4564D532688D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"29e176fbafc21491c214dd3d741c901943b17745","datavalue":{"value":"10.1007/978-3-031-27481-7_4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6174524$AB851B26-88CC-4BD5-8019-ED2378FC3B8D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"55cfbbbb889685c16294bfa3437f02f1746fc983","datavalue":{"value":{"entity-type":"item","numeric-id":352947,"id":"Q352947"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$DE92A55C-171E-4C5B-B69A-DA4E8C1DDB83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b3ad584d785cdde05d0944107b044f8c5b7dd277","datavalue":{"value":{"entity-type":"item","numeric-id":352948,"id":"Q352948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$D563A5BB-1BC0-4558-B779-5FED7078F013","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f4711e33c6ee19810f8daef27c88c57078ef6b5c","datavalue":{"value":{"entity-type":"item","numeric-id":654263,"id":"Q654263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$019A92A9-D0E1-40C4-8254-84A3816D2601","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e90650eb35b029d984e93a1c13f44e760c54facf","datavalue":{"value":{"entity-type":"item","numeric-id":352950,"id":"Q352950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$E9C394EF-0DB0-4F4F-848C-1DEE868CFEAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fa6c54e834798ee7e5695044e520626e599e9202","datavalue":{"value":{"entity-type":"item","numeric-id":6174523,"id":"Q6174523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$96F8CEB5-52F6-46D0-AE98-55E6F36FF585","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e94b967ae8cf6f3b704a08992f5caf4130874d09","datavalue":{"value":{"entity-type":"item","numeric-id":5918261,"id":"Q5918261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$8D21E42C-077C-48EE-A7A5-7F454C8C6854","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"441006eb796e3a3facfc20a479629ee7d34004ed","datavalue":{"value":{"time":"+2023-08-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6174524$5516A300-B62D-4192-97FE-4160C6C42964","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6174524$F08056BC-5FBD-412E-95D5-E10C6C17E98F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ff3eda259169ff970f6c3965a7811beb0bbcb4db","datavalue":{"value":"26A42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6174524$071170D7-9530-4C8D-B280-6681618B42EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"173ff65edcfc7a9a8461397b4283ab08ef6cd61e","datavalue":{"value":"26B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6174524$964CEDDF-8DFA-4419-ABAC-E46D991BCEF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"89fb1fcee055c06e8463e077f43859e4e2c01d9a","datavalue":{"value":"28A35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6174524$67A315E2-AA2E-4EFD-9D8F-4150807B3494","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bf858d3540da486ae72d29b0af9ac4cb0e7a8a55","datavalue":{"value":"7728835","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6174524$884F3592-EE66-4F21-89A0-9640FBE1E8FC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"326c300cf62efa849a7bdb94dd90663d744d9f5d","datavalue":{"value":"formal proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q6174524$578009E9-C5E9-4CB6-9A9A-AA75AD978777","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q6174524$BDCEE580-BF30-410F-B901-EECFC36D0FF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eae8315478af6787508c528740b602e2a5b411f4","datavalue":{"value":"measure theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6174524$EF3FAE07-9F5D-4190-83F0-D52C5939BA91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c9cf545737bba84c0c42b08aedd4ddc6b10c1df","datavalue":{"value":"Lebesgue integration","type":"string"},"datatype":"string"},"type":"statement","id":"Q6174524$4D79FE3F-B0DD-480A-BDDC-94F24F34D31C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"16ba437070a7b3a67373fbbea8e0f91dd689c150","datavalue":{"value":"Tonelli's theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q6174524$71B554D6-57BF-42A4-95FB-C96E643C9B52","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":"Q6174524$9CB4472F-B0F7-4E94-A90E-941FAA1C5275","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c7577a643cb7242f6225ccb0a4167d38e9791bea","datavalue":{"value":"https://doi.org/10.1007/978-3-031-27481-7_4","type":"string"},"datatype":"url"},"type":"statement","id":"Q6174524$17F4AF29-F669-4AA7-B547-0535304CA5AA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ca6271e33c2238f20f8d998d5d1210a52aafe3f5","datavalue":{"value":"W4310894270","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6174524$9C953329-E049-4FDE-818A-154449507F3C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f62f1315339143d3e188c7180ef4f4dd4637cfc","datavalue":{"value":{"entity-type":"item","numeric-id":2673304,"id":"Q2673304"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$980D5738-6AC0-4E6B-ABE5-34DA7A0572DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c6ecc4a9847b1757b816a66a2c8d99f5449bc756","datavalue":{"value":{"entity-type":"item","numeric-id":352952,"id":"Q352952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$59CFB631-BFB3-4D8C-B3B1-B0F890853E49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7b80111de9bab56ff28e1100701384da844fd72","datavalue":{"value":{"entity-type":"item","numeric-id":2018661,"id":"Q2018661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$8AD9E931-1591-4ADC-9077-ECA1D0DA4630","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc90f519741959885c97856c7164fc497d5566b1","datavalue":{"value":{"entity-type":"item","numeric-id":2973239,"id":"Q2973239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$FCAD8665-1FDB-4D24-841C-9B1A1005B251","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5db48c1128598242ff19c67eed4adc98aaf63b6d","datavalue":{"value":{"entity-type":"item","numeric-id":5395648,"id":"Q5395648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$9BF44BA6-8ABF-4132-9B06-1DBA30C9AB38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4977fe09e97f70b0815fbedf3e2c51a659f6429f","datavalue":{"value":{"entity-type":"item","numeric-id":2416857,"id":"Q2416857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$E26349C7-421F-4675-9E45-7E28212DA25D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c28efccb3bce398970345692451867ececf83c3a","datavalue":{"value":{"entity-type":"item","numeric-id":4910502,"id":"Q4910502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$BDC82C85-28FB-41EF-89FB-FF57E83D47D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0ef84619234e2e46e8c4513d6d1ef3cba6f5b65","datavalue":{"value":{"entity-type":"item","numeric-id":1945903,"id":"Q1945903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$52D32B73-BFED-4AC2-9381-7CEC830F50B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34dd873a66486e9e38fc156a4b8aa6ba19960bb7","datavalue":{"value":{"entity-type":"item","numeric-id":3088003,"id":"Q3088003"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$3E5BA4B5-25CF-493C-80FD-10C95296B5FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5b728d7680c9858e40e6f4070446c72d96d60c75","datavalue":{"value":{"entity-type":"item","numeric-id":3069455,"id":"Q3069455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$F989C4A4-8F87-448F-8D5C-A58676FF21E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f77a8931f2e169e40b7c98579d0d6f1bbb981a57","datavalue":{"value":{"entity-type":"item","numeric-id":5528072,"id":"Q5528072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$E30D4856-5D9A-4AA9-855E-EF7ABB6E8575","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c79ba666ab138bde3df78f585204cf8393b2232d","datavalue":{"value":{"entity-type":"item","numeric-id":6099605,"id":"Q6099605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174524$1E6D61F0-DDCE-4098-AE1B-02F4B40A4DC9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66d7a49cbc127c73bb43f0247c4df4127a92b875","datavalue":{"value":{"entity-type":"item","numeric-id":2673304,"id":"Q2673304"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8a914d7fa48ac16b4079d9d0ae743a81da264cfb","datavalue":{"value":{"amount":"+0.8718389272689819","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":"Q6174524$0AB0476B-D637-42A4-B841-53FC9475C264","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6057b5e86faf4bc8846bf7347d59327ca7961056","datavalue":{"value":{"entity-type":"item","numeric-id":5747663,"id":"Q5747663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a29de7a4a37764d7a39399214d9ee41ad5cdab2","datavalue":{"value":{"amount":"+0.7698628902435303","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":"Q6174524$C21C9813-B856-4143-9459-5B66616E0F16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"29e2d4c163df77d668e43e9741165319d047ef61","datavalue":{"value":{"entity-type":"item","numeric-id":3497625,"id":"Q3497625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"23c9e730a4267386cdca41b9045a44006f90d6bd","datavalue":{"value":{"amount":"+0.758042573928833","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":"Q6174524$D167BEC2-1B58-4D35-ACEA-43ABCB82FBC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f481d1562ef12fd442b7504ddc0be150ba4d26a6","datavalue":{"value":{"entity-type":"item","numeric-id":3088003,"id":"Q3088003"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5b60ee968952348476a2ca7525aaa5ce0f8cd873","datavalue":{"value":{"amount":"+0.7524032592773438","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":"Q6174524$D2DF7503-2B99-4C16-8D0B-70E2F8E6D785","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f7a2dfe78d9fea8f367956ae27f49fef5feb9a27","datavalue":{"value":{"entity-type":"item","numeric-id":5464655,"id":"Q5464655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea67d8b536e5ec1bdb89a907c42bf6fa037b0dd7","datavalue":{"value":{"amount":"+0.7391719222068787","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":"Q6174524$01E422C6-6490-48E8-8243-FB31C04165A8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6174524","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6174524"}}}}}