## Stream: Is there code for X?

### Topic: extend to set.insert

#### Floris van Doorn (Dec 12 2020 at 02:02):

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 (Dec 12 2020 at 02:32):

maybe something related to dfinsupp?

#### Eric Wieser (Dec 12 2020 at 08:31):

(for reference: docs#function.extend)

#### Eric Wieser (Dec 12 2020 at 08:33):

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

Last updated: May 17 2021 at 15:13 UTC