upcast `Finset (Fin n)` to `Finset (Fin n.succ)`

Stream: new members

[Becker A.]

how would I fill this out?

import Mathlib.Data.Finset.Defs

def Finset_Fin_succ
  {n : ℕ}
  (s : Finset (Fin n))
  : Finset (Fin (n + 1))
  := by sorry

[Riccardo Brasca]

You can use Fin.castSucc and Finset.image

[Riccardo Brasca]

(assuming that what you want to do is the "obvious" construction")

[Becker A.]

great, I got this:

def Finset_Fin_succ
  {n : ℕ}
  (s : Finset (Fin n))
  : Finset (Fin (n + 1))
  := by exact Finset.image Fin.castSucc s

thanks!

[Kevin Buzzard]

@Becker A. FWIW typically in Lean files : and := are on the end of the line, not the beginning, and the usual style is indent 4 not 2 before :=, so e.g.

def Finset_Fin_succ
    {n : ℕ}
    (s : Finset (Fin n)) :
    Finset (Fin (n + 1)) := by
  exact Finset.image Fin.castSucc s

although in mathlib we would probably write

def Finset_Fin_succ {n : ℕ} (s : Finset (Fin n)) : Finset (Fin (n + 1)) :=
  Finset.image Fin.castSucc s

[Becker A.]

thanks. speaking of, do you know if there's an autoformatter for Lean4 in VSCode?

[Kevin Buzzard]

This is a great question and I think that right now the answer is "not yet". You could ask about the status in #lean4 . (or just search this Zulip)

[Eric Wieser]

You could also use docs#Finset.map to get a faster implementation

[Becker A.]

okay. tried it, getting errors. how do I compose an embedding?

def Finset_Fin_succ
  {n : ℕ}
  (s : Finset (Fin n))
  : Finset (Fin (n + 1))
  := by
  apply Finset.map ?_ s
  sorry

[Becker A.]

edit: got it I think:

def Finset_Fin_succ
  {n : ℕ}
  (s : Finset (Fin n))
  : Finset (Fin (n + 1))
  := by
  apply Finset.map ?_ s
  exact Fin.castAddEmb 1

-> how is this better again, it compiles faster?

[Eric Wieser]

It #evals faster

[Eric Wieser]

map is $O(n)$, image is $O(n^2)$

[Eric Wieser]

Of course really you want this to be O(1) since this is a no-op computationally