{"entities":{"Q7361052":{"pageid":31518695,"ns":120,"title":"Item:Q7361052","lastrevid":105362519,"modified":"2026-10-07T13:34:21Z","type":"item","id":"Q7361052","labels":{"en":{"language":"en","value":"Menger's Theorem"}},"descriptions":{"en":{"language":"en","value":"AFP entry Menger"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"61b02c8492deabf88f6e7945c26c14059adfdc1b","datavalue":{"value":"https://isa-afp.org/entries/Menger.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361052$4EE13625-07A2-41BF-B389-F59925DA7568","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6c880492258c1f4e2e5bc8d3bc1bca42bfdcc3c3","datavalue":{"value":{"time":"+2017-02-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361052$17D41A2B-06EE-436F-BC32-ADDDCF461EA8","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"f49b1351385a885d620f54347daa078a5855fc73","datavalue":{"value":"Christoph Dittmann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361052$FF9BE9F0-925D-4C7C-9B94-F4B4941E60FC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8f677dd9aa01397122345e8bf96be923aacdb128","datavalue":{"value":{"text":"Menger's Theorem","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361052$679D571A-DA24-40F1-A1EA-4846D0B39A45","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a2ffea107451e0dc9628cfb0e548bb9b1c770422","datavalue":{"value":"We present a formalization of Menger's Theorem for directed and undirected graphs in Isabelle/HOL. This well-known result shows that if two non-adjacent distinct vertices u, v in a directed graph have no separator smaller than n, then there exist n internally vertex-disjoint paths from u to v. The version for undirected graphs follows immediately because undirected graphs are a special case of directed graphs.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361052$8BB57C0F-3700-463A-82B0-8A15FE5D05DE","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e65512147ed9fd828f45c7f81630112f91c614c2","datavalue":{"value":{"entity-type":"item","numeric-id":3335815,"id":"Q3335815"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361052$AA26EF38-211D-40D5-A831-C50C1166F019","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"57c86e3e3fe8d91b005219aa08ae5fddff67ae58","datavalue":{"value":{"entity-type":"item","numeric-id":1445520,"id":"Q1445520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361052$6493A05D-A7B5-4E88-ADAE-BB69332A867D","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361052$E8499D7A-882E-4662-B76C-9DC02CE7C356","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"f3718ba60fb3ca54d1e75bc16696ddd7ca207e99","datavalue":{"value":{"entity-type":"item","numeric-id":7360827,"id":"Q7360827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361052$41AF65C3-B3D9-4A29-B9A2-BEDEA208723C","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361052$1010231C-E6A5-4FCE-B4CC-FBC79CE1F8E6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Menger's Theorem","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Menger%27s_Theorem"}}}}}