{"entities":{"Q7361114":{"pageid":31518881,"ns":120,"title":"Item:Q7361114","lastrevid":105363062,"modified":"2026-10-07T13:34:45Z","type":"item","id":"Q7361114","labels":{"en":{"language":"en","value":"Matrices for ODEs"}},"descriptions":{"en":{"language":"en","value":"AFP entry Matrices_for_ODEs"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f1b41c9a57f9123ad944aa9d5d940c04d69d323d","datavalue":{"value":"https://isa-afp.org/entries/Matrices_for_ODEs.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361114$E6E64179-C323-4F9E-814F-496E926F31DC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ac0caa39db6a8090ff7712bfaef6913ff5efd66","datavalue":{"value":{"time":"+2020-04-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361114$AE67AE31-D90F-4C9D-A837-627BD09244E0","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"5794d91a39dde2e8f368834014ac9f67037fb91a","datavalue":{"value":"Jonathan Julian Huerta y Munive","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361114$00236F5C-3509-4A52-8192-E5678BC1625D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"867b7b4c63b341758e612ff2553a0c8296faa84c","datavalue":{"value":{"text":"Matrices for ODEs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361114$5DF63DC7-084B-4690-9FB8-8851CB7DF75E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"37ba2b084ff322c953ebaeca2e6fa6801d51ce9f","datavalue":{"value":"Our theories formalise various matrix properties that serve to establish existence, uniqueness and characterisation of the solution to affine systems of ordinary differential equations (ODEs). In particular, we formalise the operator and maximum norm of matrices. Then we use them to prove that square matrices form a Banach space, and in this setting, we show an instance of Picard-Lindel\u00f6f\u2019s theorem for affine systems of ODEs. Finally, we use this formalisation to verify three simple hybrid programs.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361114$A1C6E385-8D08-4762-8EC1-239428634091","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab1507b6b5edb70d4c69829a2d7e9cc7ed436f50","datavalue":{"value":{"entity-type":"item","numeric-id":832721,"id":"Q832721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361114$544BA1C5-D4B1-4ED7-A6B2-75BBA754EC3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fc62f32ebe5f2c566c09500f98ee202c262830a","datavalue":{"value":{"entity-type":"item","numeric-id":736461,"id":"Q736461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361114$1293D7D5-2B61-4486-BDE2-6781E733BE7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a3d5526333ecce1996660037c310a447acb45cd3","datavalue":{"value":{"entity-type":"item","numeric-id":5098720,"id":"Q5098720"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361114$43627E7F-7995-4A68-B944-1DB80C465F52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf2abd106579378d3a4dcae2b2666452f8595a8d","datavalue":{"value":{"entity-type":"item","numeric-id":2038037,"id":"Q2038037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361114$FFA8B1A6-B571-472B-81F0-B1579994759C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"12bcad11fe97484505c727089d3af542344d4df9","datavalue":{"value":{"entity-type":"item","numeric-id":4930176,"id":"Q4930176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361114$8A08955B-C772-451A-9827-233C95D674F6","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":"Q7361114$4DE12813-F34B-4963-96F8-FA5A28516A94","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"14bb7332ce52c95134ae033b9817ab667af44411","datavalue":{"value":{"entity-type":"item","numeric-id":7361026,"id":"Q7361026"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361114$7D031A20-3044-440B-92FA-1F2372FCE8A6","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"ef6655bf04dd34fee9f7dc3b2763244f951e30fe","datavalue":{"value":{"entity-type":"item","numeric-id":7360822,"id":"Q7360822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361114$4E8F15DE-BE54-422A-B27F-C4A5B311D814","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":"Q7361114$FF9469AB-8153-4076-9C0B-44C44DE9A3C0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Matrices for ODEs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Matrices_for_ODEs"}}}}}