function on a union

Stream: Is there code for X?

[Floris van Doorn]

Does this already exist?

variables {α β : Type*} {s t : set α}
/-- The union `f ∪ g` of two functions `f : s → β` and `g : t → β`.
  On the intersection `s ∩ t`, the function `f ∪ g` corresponds to `f`. -/
def union_elim [decidable_pred (∈ s)] (f : s → β) (g : t → β) (x : s ∪ t) : β :=
if h : (x : α) ∈ s then f ⟨x, h⟩ else g ⟨x, x.prop.resolve_left h⟩

A similar function is docs#set.piecewise.

[Eric Wieser]

There might be a version of that for subtype

[Floris van Doorn]

It's not in data.subtype at least...