Lifting is_empty instance

Stream: Is there code for X?

[Yaël Dillies]

Do we not have this anywhere?

lemma is_empty_lift {α β : Type*} [is_empty β] (f : α → β) : is_empty α :=
-- or
lemma is_empty.lift {α β : Type*} (is_empty β) (f : α → β) : is_empty α :=

[Adam Topaz]

docs#function.is_empty

[Yaël Dillies]

Ah thanks! Was looking in the wrong namespace.

[Kevin Buzzard]

I'm assuming dot notation doesn't work f.is_empty?

[Adam Topaz]

Yeah, is_empty.comap is perhaps a better name?

[Yaël Dillies]

That's what I was dreaming of.