{"entities":{"Q6860028":{"pageid":20656801,"ns":120,"title":"Item:Q6860028","lastrevid":84252188,"modified":"2026-05-14T05:36:03Z","type":"item","id":"Q6860028","labels":{"en":{"language":"en","value":"The directed Van Kampen theorem in Lean"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8158249"}},"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":"Q6860028$1646ADD2-743B-490A-8106-1C524AD1C518","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"abfa5a8efab88b19379c6787f99efeed6b8c645e","datavalue":{"value":{"text":"The directed Van Kampen theorem in Lean","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6860028$A770E375-249C-44B7-836D-4C7473FB6D26","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"950fde7bf141263c7cfae47cbbbff5d8c0ce5886","datavalue":{"value":"10.4230/LIPICS.ITP.2024.8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6860028$8E713306-DC78-486B-B592-CF8476873615","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c5c4579b04445885ccce3d16d5b0f09ea564b82d","datavalue":{"value":{"entity-type":"item","numeric-id":2233466,"id":"Q2233466"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$440D7BE9-3C76-4052-A9B8-A587CFEF3852","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2bcab3beb8add690c024b2287856825a9f13f1a9","datavalue":{"value":{"entity-type":"item","numeric-id":283908,"id":"Q283908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$EF6960F4-1E52-4A8E-8D52-8571ECE976EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"53e55cbe515cf19b1e301f8bc7a44599e4ca5231","datavalue":{"value":{"entity-type":"item","numeric-id":6860027,"id":"Q6860027"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$82E5EE7C-DAA6-4283-B90E-C1CFB79FCA9B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4f115c6be43614d2596ce7cf4daadf566de48c39","datavalue":{"value":{"time":"+2026-02-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6860028$B6B75C5C-89D5-4CA6-A940-7B552CB4DA36","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6860028$051C5F73-CA66-40F8-A61A-330F641DBD6E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4add872f22ebfdbef872ad9ceadeb1c3a2f79e53","datavalue":{"value":"8158249","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6860028$75A376B9-C639-4CB1-B761-6F9635DA6C09","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$9631D891-29E2-4BC7-A056-BDD7D97AB45D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4e8fd89fa28c0f6c3672ef10c3a2104586281edb","datavalue":{"value":"Lean","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860028$027D1316-163E-47B2-9275-49F390CAFBC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"010eb61938905ce883acf0d072b8e3f813ff6419","datavalue":{"value":"directed topology","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860028$C745194D-AFD3-468B-9E37-ABE55042EC9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"05b859aa4479069d462f60ef577ee44fe40ab261","datavalue":{"value":"Van Kampen theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860028$BC49034B-6C57-4B97-A80F-B298075688D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"699479d145ac80cd297971b1a318acf1f8c08fbb","datavalue":{"value":"directed homotopy theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860028$187BEFF3-02E1-47D4-8876-3C5AC1C68155","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c908e3891683d83ddbcdf71fc30e31eab2e1172f","datavalue":{"value":"formalised mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q6860028$EE4E9B79-19AE-426C-B6E3-26CB5817AA0C","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":"Q6860028$7F2DE495-7F1B-4413-BAA9-42FD77A78D86","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"56218d928a22983ca8dc537ad7e851b29de1654c","datavalue":{"value":{"entity-type":"item","numeric-id":5545247,"id":"Q5545247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$014891BA-4B5C-4C06-9012-DDEE20743A44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"612e554c1e5b50f840859ac28e3f2507006b7285","datavalue":{"value":{"entity-type":"item","numeric-id":5200638,"id":"Q5200638"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$8857FA34-23AF-476C-840D-C4DD8673A417","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"38c59c4f1c099bf3aa105699227af5848a751ebc","datavalue":{"value":{"entity-type":"item","numeric-id":636218,"id":"Q636218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$3845558E-57EB-4F66-B87E-A5B4EA031CBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8242928870aab67343ad0152eb7ca8357168f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$DADCE5FF-472E-4C47-BA16-6D289F504193","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9f3ae39119d06aec10527dc4783d725edc0e06e4","datavalue":{"value":{"entity-type":"item","numeric-id":1397798,"id":"Q1397798"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$2120705D-10DE-43ED-B3BD-76AA58A1FAF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3546b46a649fed581f9d6598ad032e6407f2b021","datavalue":{"value":{"entity-type":"item","numeric-id":2515156,"id":"Q2515156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$ED999805-EA9D-4E26-A414-DB3775F7D5F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9c2cbb2bf8af8fbe11bad5070e570df4153428a","datavalue":{"value":{"entity-type":"item","numeric-id":2500494,"id":"Q2500494"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$3A3DE061-9F29-47C6-BC8D-8B839D273BF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b350c5d92d979a6cbd739670641e53ab1ca0b47b","datavalue":{"value":{"entity-type":"item","numeric-id":5077344,"id":"Q5077344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$A06FBB32-1F89-44D9-8A9C-8D80443E7B01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c89d3991cde3616658992f4c69d72cb37ecc4ab6","datavalue":{"value":{"entity-type":"item","numeric-id":4453908,"id":"Q4453908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$DF341C0B-FE7D-405D-ACE8-E777BE6E0DEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"075aef123e914ffa4ca172c6bf161c17d1e17998","datavalue":{"value":{"entity-type":"item","numeric-id":3625520,"id":"Q3625520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$5DC068CC-E7A9-4AF2-B689-E06720C2BC62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aa5c7d5ef5c850ae0c8c6c7e82814cd77a617bd7","datavalue":{"value":{"entity-type":"item","numeric-id":5278408,"id":"Q5278408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$AB0D46C1-AAEF-48E2-90F9-F3CED677A6D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"703b375661ad591494ac18fba9521d92e800405a","datavalue":{"value":{"entity-type":"item","numeric-id":1037410,"id":"Q1037410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$D1A19DE9-8087-45F3-9BE0-B85E8DE78DCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9e1d062d881e28f4fc6b4153c0765dec6b39a1b4","datavalue":{"value":{"entity-type":"item","numeric-id":5170245,"id":"Q5170245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$B4C27FB8-6399-4F22-9FB3-AC34D311CF51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"320be0100130068b2dc0b1290f4357d23b143166","datavalue":{"value":{"entity-type":"item","numeric-id":4064159,"id":"Q4064159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$B8208B99-4C76-4FA9-9002-DA5DAA0B7723","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19a5d4ac1c8b434a0d89267cd5b7138fc554dd4b","datavalue":{"value":{"entity-type":"item","numeric-id":1687770,"id":"Q1687770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$E5DBBB9C-C798-438B-9AB2-9F59C400CF11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a3916113c855be09ff7c725f2222d49866271f77","datavalue":{"value":{"entity-type":"item","numeric-id":2491631,"id":"Q2491631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6860028$A7ED6BE7-268A-4B70-80EB-7EB2335EE49C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The directed Van Kampen theorem in Lean","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_directed_Van_Kampen_theorem_in_Lean"}}}}}