Zulip Chat Archive

Stream: Is there code for X?

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


view this post on Zulip 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 }

view this post on Zulip 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