{"entities":{"Q1687728":{"pageid":1698469,"ns":120,"title":"Item:Q1687728","lastrevid":71999718,"modified":"2026-04-14T01:59:31Z","type":"item","id":"Q1687728","labels":{"en":{"language":"en","value":"A formal proof in Coq of Lasalle's invariance principle"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6821849"}},"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":"Q1687728$98B7BA4D-43BA-4FAE-8EE7-65F44518F3BC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fa78aaab7c5370e57caec845b714220e5e879798","datavalue":{"value":{"text":"A formal proof in Coq of Lasalle's invariance principle","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1687728$6BCD09E2-9DE0-403C-ACB3-3F89273BB3AA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"21d79230722e539cd505f75456f07353882ced76","datavalue":{"value":"1484.68315","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687728$0F2A4422-5B46-4166-A096-25FCD5529829","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d22776ed3ffb9318bee5dde803303167401729fa","datavalue":{"value":"10.1007/978-3-319-66107-0_10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687728$34F8E592-1585-48DE-BF18-57D20A15B591","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"110c9b9e0e852b5bffe2fcd42275bf67a9f49ee7","datavalue":{"value":{"entity-type":"item","numeric-id":375195,"id":"Q375195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$E4C441FF-4951-424F-BEF6-50D34A4C1EB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"21a01fed6e1c276e027d0f9654129a6fafd984e7","datavalue":{"value":{"entity-type":"item","numeric-id":1687727,"id":"Q1687727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$C7781795-FB52-4895-A20C-7F4C31D7DBD6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7600255b4ee907c1b1dfbc5f62c7b1165ab1b6d0","datavalue":{"value":{"time":"+2018-01-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1687728$6632B2CB-2F14-477B-9EC3-7C00F5539091","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fa5c51c08615750def38d6020c72e41c91fe40c4","datavalue":{"value":"https://hal.inria.fr/hal-01612293/file/main.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q1687728$83826C88-866E-4539-A682-B771C7CC9C32","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687728$AE6DC196-A584-4326-A46E-F83768A7BFC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"081a4b535274c822e812aa844182821199bda85b","datavalue":{"value":"34D20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687728$3EDA0420-286A-41A8-A4BE-8048D28422C7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"282ee6bcc6765081376700b6fa5a4cb6f8fc66b2","datavalue":{"value":"6821849","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687728$D026D026-37BC-4D99-803C-17BA0EA73B59","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"55caf05c57404ab910cf1d6d785d791abcc73ea3","datavalue":{"value":"formal proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1687728$942DC9D1-C449-4F9E-B4BD-55869BA03646","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q1687728$F783934F-E633-4682-9940-4C9B499DF26A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"554ce1904bc7aad8ab28dec67ee5f4a3db655bbe","datavalue":{"value":"dynamical systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1687728$280DB367-19AD-46AF-BAC4-D121523D469C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"34b44e7b40021effdee26093512bde7058814281","datavalue":{"value":"stability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1687728$8A7E1104-A703-4EC1-885E-F876EA431CCA","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"84eefd31cc35b0f322abc9d88353a26c9605ee67","datavalue":{"value":{"entity-type":"item","numeric-id":23492,"id":"Q23492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$426049B9-6B88-4A8D-B653-CA0F9FC71AE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$0EEF12B9-AA6E-4B14-B2E6-BA93B67C8982","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$4DDC9B08-6685-4CD3-9074-F18DFBEE642D","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":"Q1687728$0B42400B-6F93-466B-932B-D66EBFD51E17","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"12c140b1655c31965ff8d402cfaac8d9fb9a8432","datavalue":{"value":"W2745776412","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687728$0B1882D4-70E3-40FD-A294-A45F9111D7A2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"565dcdf804604f5e5a70c48937ec7dfa7182199d","datavalue":{"value":{"entity-type":"item","numeric-id":5265669,"id":"Q5265669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$BA372D14-0E9B-4DBB-94FD-A2B6524B07D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf446b5419b8e3a70a44aff75bbc12fa8bd693c8","datavalue":{"value":{"entity-type":"item","numeric-id":2391534,"id":"Q2391534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$1720D083-AEA2-42B7-9752-2AE774FAD1AB","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":"Q1687728$AECFCEC6-590B-4AA2-B8BC-E7BFB4FC9163","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"48f442a15050db414e2e141a1d0a71d0d3383b1e","datavalue":{"value":{"entity-type":"item","numeric-id":5958820,"id":"Q5958820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$5B035A38-873F-470E-A46A-438FA16EC630","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c80ecc04876d198f70a708fe539b750f5b853134","datavalue":{"value":{"entity-type":"item","numeric-id":5353336,"id":"Q5353336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$26652899-72F0-41CF-B5CE-780C915742D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d9190693f3924b86be7203c014f0b8b161bc6f8","datavalue":{"value":{"entity-type":"item","numeric-id":5302559,"id":"Q5302559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$4777DA1D-E208-4A97-82E0-DECDC699BF92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7dac16af6cf1adb18d0516e2c8db27f45fc424e6","datavalue":{"value":{"entity-type":"item","numeric-id":5327343,"id":"Q5327343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$8B0C68C4-51DD-4FEC-92A3-1D6D109050B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d360f4c10b4163627f57faa3db163275ea6a011","datavalue":{"value":{"entity-type":"item","numeric-id":5327350,"id":"Q5327350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$DCA40377-151F-4876-82A6-C2B8F2E6C64A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f2c6a4e3245926b8c81e177c391cd48c1834463","datavalue":{"value":{"entity-type":"item","numeric-id":1575420,"id":"Q1575420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$AA8F263D-C302-4F6F-9736-5A985F172EAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"23556da57666c49b7b15a4150a20d305eea7d81e","datavalue":{"value":{"entity-type":"item","numeric-id":2504673,"id":"Q2504673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$E7E964FC-217D-4CD4-9265-10D9E57D8846","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8b46b970d8ad468e53da493354fcb3e5cd79f65","datavalue":{"value":{"entity-type":"item","numeric-id":3543661,"id":"Q3543661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$D995FA63-7DB3-4D3D-9CFF-933BE540FCC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8fdf8dff45f462e3d337fa5891b679db6ae2101a","datavalue":{"value":{"entity-type":"item","numeric-id":5637596,"id":"Q5637596"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687728$87BED330-BC2F-4FCD-9A1A-A5733042A1BB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d829aeb5c94bc0b54a7d6acc8f145678fbef8cf3","datavalue":{"value":{"entity-type":"item","numeric-id":681340,"id":"Q681340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae0f991f192828550eda62858876af49b98f2ed0","datavalue":{"value":{"amount":"+0.7070474624633789","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":"Q1687728$8F50A050-9024-48C0-AD3E-211396B02BF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0ad6036a0d30e0a5e0065d8b4d7fd2456e2c17bc","datavalue":{"value":{"entity-type":"item","numeric-id":5172656,"id":"Q5172656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4eb7c48538f49d678970b1448dd80049e1da0a86","datavalue":{"value":{"amount":"+0.7058896422386169","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":"Q1687728$BFC3C5AA-49EF-4DCF-BB72-072B59501FDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e6eb9aa5d44ce8435856c5ab534b0bf4df0d4612","datavalue":{"value":{"entity-type":"item","numeric-id":2233505,"id":"Q2233505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ccb44a6b0f631cd4c35d9611785841c38fefa1eb","datavalue":{"value":{"amount":"+0.7017518281936646","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":"Q1687728$9137E355-8C1B-407C-AA96-1DDE0B1C8924","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d822b8b30ac1f0628d274d8d49a837f75fa8920","datavalue":{"value":{"entity-type":"item","numeric-id":1861861,"id":"Q1861861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f98cda00bcbeb87692b1e080968d1cc6326e10b0","datavalue":{"value":{"amount":"+0.7009638547897339","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":"Q1687728$8C5AB251-8942-45FB-BFAD-F186C039A95A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39238a54e13d47fec1b12ebdaf4bdde91a595b7d","datavalue":{"value":{"entity-type":"item","numeric-id":1770230,"id":"Q1770230"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fda77a53876ec482910f38426b0fe5e3da53acdd","datavalue":{"value":{"amount":"+0.6981215476989746","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":"Q1687728$699D65BF-6B97-41BE-A90F-2E88441D51AB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A formal proof in Coq of Lasalle's invariance principle","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_formal_proof_in_Coq_of_Lasalle%27s_invariance_principle"}}}}}