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 con
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 Coll
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 fr
