extend to set.insert

Stream: Is there code for X?

[Floris van Doorn]

Does this function already exist?

import data.set.basic

noncomputable theory
open set
open_locale classical

namespace function

variables {ι : Type*} {α : ι → Type*} {s : set ι} {i : ι}

def extend_insert (f : Π (j : ι), j ∈ s → α j) (x : α i) (j : ι) (hj : j ∈ insert i s) : α j :=
if h : j = i then by { subst h, exact x } else f j (mem_of_mem_insert_of_ne hj h)

end function

Even though it looks similar, it is not a special case of function.update or function.extend.

[Kenny Lau]

maybe something related to dfinsupp?

[Eric Wieser]

(for reference: docs#function.extend)

[Eric Wieser]

It looks like function.extend is missing a generalization to dependent functions perhaps; which if it had, I think would work for your case if expressed with subtypes