Define function with narrower range

Stream: new members

[Abdullah Uyu]

I defined a function that returns a Set G, and I proved that that Set G is a subset of star (ell := ell) b c. But I want the return type to be star (ell := ell) b c. How can I achieve that?

import Mathlib.Tactic

variable [DecidableEq G]

open Set
namespace Basic

def star
  (ell : G → G → G → Prop)
  (a b : G) :
    Set G :=
  {c : G | if a = b then c = a else ell a b c}

def central_projection
  (a b c z: G)
  (ell : G → G → G → Prop)
  (x : star (ell := ell) a c) :
    Set G :=
  star (ell := ell) x z ∩ star (ell := ell) b c

theorem cen_proj_in_line
  (a b c z : G)
  (x : star (ell := ell) a c) :
    central_projection (ell := ell) a b c z x ⊆ star (ell := ell) b c := by
  unfold central_projection
  rw [subset_def (s := star (ell := ell) x.val z ∩ star (ell := ell) b c) (t := star (ell := ell) b c)]
  intro xx xx_in_inter
  exact mem_of_mem_inter_right xx_in_inter

def central_projection'
  (a b c z: G)
  (ell : G → G → G → Prop)
  (x : star (ell := ell) a c) :
    star (ell := ell) b c :=
  -- star (ell := ell) x z ∩ star (ell := ell) b c
  -- How to fill here?

[Kevin Buzzard]

You seem to want the return type of central_projection' to be star (ell := ell) b c, which is a term (it's a set), so Lean promotes it to a type and thus wants central_projection' ... to be a term of type ↑(star ell b c). To make a term of this type you need to give a pair ⟨g, hg⟩ with g : G and hg : g ∈ star ell b c. In particular I'm not clear about what you want to do with the set star (ell := ell) x z ∩ star (ell := ell) b c -- Lean wants an element, not a subset, here, the way you've set things up.

[Abdullah Uyu]

Right, I see. Now I am a bit confused if I should have said Set (star (ell := ell) b c.

[Abdullah Uyu]

I should think about it a little bit.

[Kevin Buzzard]

Oh then maybe you want

def central_projection'
    (a b c z: G)
    (ell : G → G → G → Prop)
    (x : star ell a c) :
    Set (star ell b c) := Subtype.val ⁻¹' (star ell x z ∩ star ell b c)

(by the way I removed all the ell := ell stuff, I don't know why you're writing it like that)

[Abdullah Uyu]

Aha! That's it, thank you! As for ell := ell, I realize I was blindly writing that for star, but it makes a difference for some other functions. I guess it's because of some parameter subject that I should study more carefully.

[Kevin Buzzard]

ell is an explicit input to your function (round brackets (...)) so you can just give it. It's only when a function has an implicit input {ell} that you need this notation.