Coercion of SetLike-valued functions to Set-valued functions

Stream: new members

[Evan Bailey]

I was wondering if there is any reason why Mathlib doesn't have a coercion from SetLike-valued functions to Set-valued functions. For example, something like the following:

import Mathlib.Data.FunLike.Basic
import Mathlib.Data.SetLike.Basic
universe u₁ u₂ u₃
variable (α : Sort u₁) (β : α → Type u₂) (γ : α → Type u₃) [∀ a, SetLike (β a) (γ a)]
instance (priority := 100) instDFunLikeSetLike : DFunLike (∀ a, β a) α (Set ∘ γ) where
  coe f a              := SetLike.coe (f a)
  coe_injective' _ _ h := funext fun a ↦ SetLike.coe_injective (congrFun h a)

I am not familiar enough with the details of typeclass inference to know whether this would cause problems or slowdowns. My current understanding is that it would not. Since the second and third parameters of DFunLike are outParams, Lean should only attempt to instantiate this if it already knows the first argument. In this case, it already knows α and β, from which it can infer γ using the SetLike instance. However, I am interested to hear if my understanding is not correct.

The motivation behind this question is to enable things like this:

import Mathlib.Topology.Sets.Closeds
open scoped Topology

variable {X : Type u₂} {Y : Type u₃} [TopologicalSpace X] [τY : TopologicalSpace Y]
def UpperHemicontinuous (f : X → Set Y) : Prop :=
  ∀ x (s : τY.Opens), f x ⊆ s → ∀ᶠ x' in 𝓝 x, f x' ⊆ s

/-- Part of the Closed Graph Theorem for X → Set Y -/
theorem closed_graph_of_closed_of_upperHemicontinuous [T2Space Y] [CompactSpace Y] {f : X → Set Y}
    (cl : ∀ x, IsClosed (f x)) (uhc : UpperHemicontinuous f) : IsClosed {(x, y) | y ∈ f x} := sorry
/-- Part of the Closed Graph Theorem for X → τY.Closeds -/
theorem closed_graph_of_closed_of_upperHemicontinuous' [T2Space Y] [CompactSpace Y]
    {f : X → τY.Closeds} (uhc : UpperHemicontinuous f) : IsClosed {(x, y) | y ∈ f x} :=
  closed_graph_of_closed_of_upperHemicontinuous (f · |>.closed) uhc