Continuous empty map

Stream: Is there code for X?

[Nicolò Cavalleri]

Do we have somewhere that the empty map from the empty type to the empty type is continuous? I'd need to prove the continuity of a map that looks like

continuous (λ x : α, _.elim)

[Adam Topaz]

import topology.constructions

example {α : Type*} [topological_space α] (f : pempty → α) : continuous f := continuous_bot

[Adam Topaz]

(found using library_search)

[Adam Topaz]

Oh to the empty type! Sorry, I misread

[Yaël Dillies]

Endomorphism of the empty type. This really has to be some formalization nonsense :stuck_out_tongue_closed_eyes:

[Adam Topaz]

It would be helpful to know how you have this formulated. e.g.

import topology.constructions

example {α β : Type*} [is_empty β] [topological_space α] [topological_space β]
  (f : α → β) : continuous f :=
by { letI := function.is_empty f, exact continuous_of_discrete_topology }

[Vasu]

Thanks for showing how to use example, I was confused I was using #example