Ascoli-Arzelà theorem

DOI10.2478/forma-2021-0009zbMath1483.68496OpenAlexW4206292958MaRDI QIDQ2119549

Keiichi Miyajima, Yasunari Shidama, Hiroshi Yamazaki

Publication date: 29 March 2022

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

Full work available at URL: https://doi.org/10.2478/forma-2021-0009

zbMATH Keywords

Ascoli-Arzela's theoremequiboundedness of continuous functionsequicontinuousness of continuous functions

Mathematics Subject Classification ID

Compactness in Banach (or normed) spaces (46B50) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Mizar

Cites Work

• The role of the Mizar mathematical library for interactive proof development in Mizar
• Functional space consisted by continuous functions on topological space
• Mizar: State-of-the-art and Beyond
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item