Zulip Chat Archive

Stream: Is there code for X?

Topic: Right inverse of injective


Pedro Minicz (Jul 24 2020 at 17:25):

Is there something equivalent to right_inverse_of_injective in mathlib?

import tactic.basic

variables {α β : Type} [nonempty α] {f : α  β}

lemma right_inverse_of_injective (hf : function.injective f) :
   g, function.right_inverse f g :=
begin
  classical,
  let g := λ b,
      if h :  a, f a = b
        then classical.some h
        else classical.choice (by apply_instance),
  use g,
  intro a,
  have ha :  a', f a' = f a, from a, rfl,
  simp only [g, dif_pos ha],
  apply hf,
  exact classical.some_spec ha
end

Reid Barton (Jul 24 2020 at 17:30):

left_inverse_inv_fun

Reid Barton (Jul 24 2020 at 17:34):

or even injective.has_left_inverse


Last updated: Dec 20 2023 at 11:08 UTC