Now f is continuous (exercise!)
Arthan, Robin Denis
Journal of Formalized Reasoning, Volume 9 (2016), / Harvested from Journal of Formalized Reasoning

A recurring proof obligation in modern mathematics, ranging from textbook exercises to deep research problems, is to show that a given function is a morphism in some category: in analysis and topology, for example, we frequently need to prove that functions are continuous, while in group theory we are constantly concerned with homomorphisms. This paper describes a generic procedure that automatically discharges routine instances of this kind of proof obligation in an interactive theorem prover. The proof procedure has been implemented and found very useful in a mathematical case studies carried out using the ProofPower system

Published online : 2016-01-01
     title = {Now f is continuous (exercise!)},
     journal = {Journal of Formalized Reasoning},
     volume = {9},
     year = {2016},
     doi = {10.6092/issn.1972-5787/4566},
     language = {EN},
     url = {}
Arthan, Robin Denis. Now f is continuous (exercise!). Journal of Formalized Reasoning, Volume 9 (2016) . doi : 10.6092/issn.1972-5787/4566.