Zulip Chat Archive

Stream: Is there code for X?

Topic: extend to set.insert

view this post on Zulip Floris van Doorn (Dec 12 2020 at 02:02):

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.

view this post on Zulip Kenny Lau (Dec 12 2020 at 02:32):

maybe something related to dfinsupp?

view this post on Zulip Eric Wieser (Dec 12 2020 at 08:31):

(for reference: docs#function.extend)

view this post on Zulip 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