Re: [isabelle-dev] Redundant definitions in Analysis
Le 11/03/2019 à 19:13, Fabian Immler a écrit : Sébastien might have a stronger opinion (I don't), but I would also go for continuous_map: it is in line with open_map, closed_map, quotient_map (which we don't have as constants, but use in theorem names). Moreover, we have more occurrences of continuous_map (174+0 vs 83+39 in isabelle+AFP). You can definitely go for continuous_map. Best, Sebastien ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Redundant definitions in Analysis
On 3/7/2019 7:36 AM, Lawrence Paulson wrote: 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. Sébastien might have a stronger opinion (I don't), but I would also go for continuous_map: it is in line with open_map, closed_map, quotient_map (which we don't have as constants, but use in theorem names). Moreover, we have more occurrences of continuous_map (174+0 vs 83+39 in isabelle+AFP). Fabian smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Redundant definitions in Analysis
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. Any comments? Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev