[isabelle-dev] Redundant definitions in Analysis
lp15 at cam.ac.uk
Thu Mar 7 13:36:36 CET 2019
In Analysis, we have two equivalent definitions of continuous functions between two topological spaces:
lemma "continuous_map X Y f = continuous_on_topo X Y f"
by (auto simp add: continuous_map_def continuous_on_topo_def vimage_def image_def Collect_conj_eq inf_commute)
The first one comes from HOL Light and is defined in Abstract_Topology. The latter is declared in Function_Topology.
Obviously we need to eliminate one of them, and I prefer the former name. The latter is more logical but clunky, especially when compound with others in theorem names.
More information about the isabelle-dev