{"entities":{"Q6534204":{"pageid":14145271,"ns":120,"title":"Item:Q6534204","lastrevid":54618635,"modified":"2026-01-29T18:46:55Z","type":"item","id":"Q6534204","labels":{"en":{"language":"en","value":"Metric spaces are paracompact"}},"descriptions":{},"aliases":{},"claims":{"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"30e8d878139f2091943264fb4bf799c9637c746e","datavalue":{"value":{"entity-type":"item","numeric-id":6534201,"id":"Q6534201"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6534204$0bfa7164-4c9d-661f-1bcb-7c290b30c1ab","rank":"normal"}],"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"c8566a493116758818d5a26d859f86220f609b7b","datavalue":{"value":{"entity-type":"item","numeric-id":6480412,"id":"Q6480412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6534204$e429741b-4306-a1ea-6917-c10b19c9e8b5","rank":"normal"}],"P104":[{"mainsnak":{"snaktype":"value","property":"P104","hash":"79c2dceb45e851f22d76be79fd1bd9908514dc64","datavalue":{"value":"https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/EMetricSpace/Paracompact.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q6534204$e94a7cc3-414d-5bf4-b649-05d4197b182e","rank":"normal"}],"P1459":[{"mainsnak":{"snaktype":"value","property":"P1459","hash":"124758e47d2c09d51203c580a86778abbf7396e5","datavalue":{"value":"Every extended metric space (e-metric space) is paracompact. Specifically, for any open cover of an e-metric space, there exists a locally finite open refinement. This theorem guarantees that extended metric spaces satisfy a fundamental property in topology, making them suitable for applications requiring locally finite refinements of open covers.","type":"string"},"datatype":"string"},"type":"statement","id":"Q6534204$20e24896-4113-5b5e-9e1a-28db3e97016b","rank":"normal"}],"P1648":[{"mainsnak":{"snaktype":"value","property":"P1648","hash":"65a1fd7ab95adf47bffa0d77deeda084e54d0941","datavalue":{"value":{"entity-type":"item","numeric-id":52541,"id":"Q52541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P132":[{"snaktype":"value","property":"P132","hash":"7aecacf3ec16503e9d216f82ecca8dc24a39170b","datavalue":{"value":"v4.14.0","type":"string"},"datatype":"string"}]},"qualifiers-order":["P132"],"id":"Q6534204$d712ba17-464c-20c1-b884-b38eafccfed7","rank":"normal","references":[{"hash":"6384c45fe3787d01fbbe5b7f0779333715ed2ae8","snaks":{"P56":[{"snaktype":"value","property":"P56","hash":"8c0172429067064b73f0e33e3e2d96819f7eb2a9","datavalue":{"value":"https://github.com/leanprover-community/mathlib4/blob/v4.14.0/Mathlib/Topology/EMetricSpace/Paracompact.lean#L37C28-L37C37","type":"string"},"datatype":"url"}]},"snaks-order":["P56"]}]}]},"sitelinks":{"mardi":{"site":"mardi","title":"Metric spaces are paracompact","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Metric_spaces_are_paracompact"}}}}}