A formalization of metric spaces in HOL Light
From MaRDI portal
Publication:682381
DOI10.1007/s10817-017-9412-xzbMath1425.68376OpenAlexW2289810656MaRDI QIDQ682381
Publication date: 2 February 2018
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-017-9412-x
Related Items
The flow of ODEs: formalization of variational equation and Poincaré map, From types to sets by local type definition in higher-order logic, Quantitative continuity and Computable Analysis in Coq
Uses Software
Cites Work