injective on `some`

Stream: new members

[Horatiu Cheval]

I have a function f : α → option β and I want to say "f is injective on those arguments mapped to some and I don't care what happens with those mapped to none". Basically this:

def inj_some {α β : Type} (f : α → option β) : Prop :=
  ∀ x y : α, (f x).is_some → (f y).is_some → f x = f y → x = y

Does this have a name or is an instance of a more general notion in Lean?

[Mario Carneiro]

I have definitely had use for this condition before, but only rarely, and so it is just written out where it is used. You can see the usual way it is written in docs#list.nodup_filter_map or docs#pequiv.inj

[Mario Carneiro]

(note that b ∈ f a on option means f a = some b)

[Eric Wieser]

Does (set.range option.some).inj_on f work for you?

[Mario Carneiro]

That requires that f : option α → β and says that f is injective on the some part of its domain. We want the opposite: f is injective if it maps into the some part of the codomain

[Mario Carneiro]

you could write it with inj_on as (f ⁻¹' set.range option.some).inj_on f but I'm not sure that's better than just writing it out