Subtypes of functions are equivalent to functions to subtype

Stream: Is there code for X?

[Eric Wieser]

Do we have something like this?

/-- Functions whose range lies within a set are equivalent to functions to that set. -/
def foo (α : Type*) {β : Type*} (bs : set β) :
  {f : α → β // set.range f ⊆ bs} ≃ (α → bs) :=
{ to_fun := λ f a, set.cod_restrict f bs $ λ x, f.prop (set.mem_range_self x),
  inv_fun := λ f, ⟨_, λ  _ ⟨a, ha⟩, ha ▸ (f a).prop⟩,
  left_inv := λ x, by { ext, refl },
  right_inv := λ x, by { ext, refl } }

[Eric Wieser]

Or equivalently using docs#subtype.coind:

def subtype.coind_equiv (α : Type*) {β : Type*} (p : β → Prop) :
  {f : α → β // ∀ a, p (f a)} ≃ (α → subtype p) :=
{ to_fun := λ f, subtype.coind (f : α → β) f.2,
  inv_fun := λ f, ⟨coe ∘ f, λ a, (f a).prop⟩,
  left_inv := λ x, subtype.ext $ rfl,
  right_inv := λ x, funext $ λ _, subtype.ext rfl }