## Stream: Is there code for X?

### Topic: left_inverse imples  α ≃ set.range f

#### Eric Wieser (Mar 22 2021 at 16:26):

Do we have a computable version of docs#equiv.set.range?

def function.left_inverse.equiv_range {α β : Sort*} {f' : β → α} {f : α → β} (hf : function.left_inverse f' f):
α ≃ set.range f :=
{ to_fun := λ a, ⟨f a, a, rfl⟩,
inv_fun := λ b, f' b,
left_inv := hf,
right_inv := λ ⟨b, a, ha⟩, subtype.eq \$ show f (f' b) = b,
from (ha ▸ hf a : f' b = a).symm ▸ ha }


#### Eric Wieser (Mar 22 2021 at 18:09):

I'll take silence as "no", pr'd as #6821. We have similar definitions as docs#linear_equiv.of_left_inverse and docs#ring_equiv.of_left_inverse, so I went for the name equiv.set.range_of_injective

Last updated: May 17 2021 at 15:13 UTC