Idiomatic way to deal with irrelevant part of domain

Stream: mathlib4

[Pim Otte]

This is a problem I've been running into every once in a while. As an example, I'm defining a way to get a subgraph from a function, where the edges are between nodes and whatever the function maps them to.

def Subgraph.ofFunction {u : Set V} (f : V → V) (h : ∀ v ∈ u, G.Adj v (f v)) : Subgraph G where
  verts := u ∪ f '' u
  Adj v w := v ∈ u ∧ f v = w ∨ w ∈ u ∧ f w = v
  adj_sub := by
    intro v w' hvw'
    cases' hvw' with hv hw'
    · rw [← hv.2]
      exact h v hv.1
    · rw [← hw'.2]
      exact (h w' hw'.1).symm
  edge_vert := by
    intro v w hvw'
    cases' hvw' with hv hw'
    · left; exact hv.1
    · right; rw [← hw'.2]
      exact Set.mem_image_of_mem f hw'.1

In this example, I've defined f : V → V, because that works out nicely with typechecking, even though the domain outside of u doesn't really matter at all. The problem is that when using this you do need to define the whole function. I've done this before by just using an if/else and some junk element in the case where we're not in u, but this seems horribly hacky.

Is there an idiomatic way to deal with this? Should my definition be using f : u → V? Or is there a way to cleanly extend a function from u → V to V → V?

[Yaël Dillies]

You can use docs#Function.extend, but I would consider your original approach as fine