The linearity of Riemann integral on functions from \(\mathbb{R}\) into real Banach space

DOI10.2478/forma-2013-0020zbMath1298.26031MaRDI QIDQ467790

Yasunari Shidama, Noboru Endou, Keiko Narita

Publication date: 5 November 2014

Published in: Formalized Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2478/forma-2013-0020

zbMATH Keywords

formalization of Riemann integral

Mathematics Subject Classification ID

26A42: Integrals of Riemann, Stieltjes and Lebesgue type

03B35: Mechanization of proofs and logical operations