Defining function on union

Stream: Is there code for X?

[Chris Hughes]

Is there an interface for defining a function on the union of sets given functions on each of the individual sets that agree where necessary?

[Adam Topaz]

I don't know, but just wanted to mention that there was a discussion on gluing continuous functions that seems related.

[Adam Topaz]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/partial.20functions.20and.20gluing/near/251825197

[Adam Topaz]

Looks like it doesn't answer your question though. Sorry

[Eric Wieser]

Your question is the same as (f : subtype p → A) (g : subtype q → A) (∀ x (hp : p x) (hq : q x), f x = g x) : subtype (p ⊔ q) → A, right?

[Chris Hughes]

Yes, but on arbitrary unions not just binary unions.

[Kevin Buzzard]

You want to prove the presheaf is a sheaf

[Eric Wieser]

So (f : Π i, subtype (p i) → A) (∀ x i j, p i x → p j x → f i x = f j x) : subtype (⨆ i, p i) → A, right?

[Chris Hughes]

Yes

[Kevin Buzzard]

A-valued functions on subsets of a set are a sheaf: this is precisely the statement that given f i as above there's a unique f which restricts to the f i. This doesn't help with the proof but it's a nice basic example of a sheaf so I thought I'd mention it.

[Chris Hughes]

Surprisingly, Lean didn't ask me to mark this as noncomputable. I guess it must be impossible to constructively define an f that doesn't agree on the intersections.

def Union_map (S : set (set α))
  (f : Π (s ∈ S) (x ∈ s), β x)
  (hf : ∀ s (hs : s ∈ S) t (ht : t ∈ S) (x : α) (hxs : x ∈ s) (hxt : x ∈ t),
    f s hs x hxs = f t ht x hxt) :
  Π x, x ∈ ⋃₀ S → β x :=
λ x hx,
let s : set α := classical.some hx in
have hs : s ∈ S ∧ x ∈ s := exists_prop.1 (classical.some_spec hx),
f s hs.1 x hs.2

[Eric Wieser]

Sounds like you either have noncomputable theory in your preamble or accidentally remained in Prop.

[Chris Hughes]

No, it's computable. You're allowed classical.choice to choose a Type or a Prop since there are no computable non-constant functions from Type or Prop into a normal computable Type like nat anyway. IIRC, Type and Prop are represented as unit in the VM.

[Chris Hughes]

#9019

[Kevin Buzzard]

Nice!