Convert functions between subsets to functions between types

Stream: Is there code for X?

[Wen Yang]

I find it more convenient to work on types than subtypes in Lean. However, some functions are naturally defined on subsets, which are defined as subtypes. Therefore, I hope there is a natural way to convert these functions to functions defined on types. I don't know if there is already a solution in mathlib4, at least I didn't find one. So I wrote one and submitted a PR. The main definition is as follows:

import Mathlib.Topology.ContinuousOn
set_option autoImplicit true
open Set Function
variable {s : Set α} {t : Set β} [Nonempty ↑t] [DecidablePred (· ∈ s)]

noncomputable def Function.toval (f : s → t) [DecidablePred (· ∈ s)] : α → β := by
  have ht : Set.Nonempty t := by rw [← @nonempty_coe_sort]; assumption
  let y := ht.some
  exact fun x =>
    if hx : x ∈ s then (f ⟨x, hx⟩).val
    else y

See https://github.com/leanprover-community/mathlib4/pull/7449 for more details.
I wonder if we could add this to mathlib4.

[Yaël Dillies]

You could use docs#Function.extend. Precisely, Function.toval f = Function.extend f fun _ ↦ (Set.nonempty_coe_sort.1 ‹_›).some.

[Wen Yang]

Thanks, Yaël Dillies. Unfortunately, Function.extend f fun _ ↦ (Set.nonempty_coe_sort.1 ‹_›).some did not work.​ I think it's not intuitive to use Function.extend here.

[Yaël Dillies]

Ah sorry I just forgot an argument to Function.extend. Replace Function extend f by Function.extend Subtype.val f.

[Yaël Dillies]

I wonder why it's not intuitive though. You want to extend a function defined on s to a function defined on the full domain α. Is that not intuitive?

[Wen Yang]

Maybe I'm just not used to it yet. This works:

import Mathlib.Data.Set.Basic
set_option autoImplicit true
open Set Function
variable {s : Set α} {t : Set β} [Nonempty ↑t]

noncomputable def Function.toval (f : s → t) : α → β :=
    extend Subtype.val
    (Subtype.val ∘ f)
    (fun _ ↦ (Set.nonempty_coe_sort.1 ‹_›).some)

[Wen Yang]

I'll try to see if I can build the APIs for this.

[Wen Yang]

I have modified the definition of Function.toval. However, I don't know how to work with Function.extend, so I give up. I don't even know how to prove that the two definitions are the same:​

import Mathlib.Data.Set.Function
set_option autoImplicit true
open Set Function
variable {s : Set α} {t : Set β} [Nonempty β]

noncomputable def Function.toval (f : s → t) : α → β :=
  fun x =>
    haveI : Decidable (x ∈ s) := Classical.propDecidable _
    if hx : x ∈ s then (f ⟨x, hx⟩).val
    else Classical.choice ‹_›

theorem toval_eqOn_extend {f : s → t} : EqOn
    f.toval
    (extend Subtype.val
      (Subtype.val ∘ f)
      (fun _ ↦ Classical.choice ‹_›))
    s := by sorry

[Yaël Dillies]

Here's a proof:

import Mathlib.Data.Set.Function
set_option autoImplicit true
open Set Function
variable {s : Set α} [Nonempty β]

noncomputable def Function.toval (f : s → β) : α → β :=
  fun x =>
    haveI : Decidable (x ∈ s) := Classical.propDecidable _
    if hx : x ∈ s then f ⟨x, hx⟩
    else Classical.choice ‹_›

theorem toval_eq_extend {f : s → β} :
    extend Subtype.val f (fun _ ↦ Classical.choice ‹_›) = f.toval := by
  ext a
  unfold toval
  split_ifs with ha
  · exact Subtype.val_injective.extend_apply _ _ (⟨a, ha⟩ : s)
  · refine extend_apply' _ _ _ ?_
    rintro ⟨a, rfl⟩
    exact ha a.2

[Wen Yang]

@Yaël Dillies Thank you very much! I have submitted a PR that includes your proof: https://github.com/leanprover-community/mathlib4/pull/7482