Union of k sets

Stream: new members

[Eric Wieser]

If I have a function f : nat -> set T, is there a better way of spelling fs_up_to in the following?

def f : nat -> set α := sorry
def fs_up_to (k : ℕ) := ⋃ (s : {s : ℕ // s <= k}), f s

Using subtypes feels a little awkward

[Eric Wieser]

Is a recursive definition using set.union likely to be easier to make statements about?

[Alistair Tucker]

Your definition by subtype already exists in core https://github.com/leanprover/lean/blob/master/library/init/data/fin/basic.lean

[Kevin Buzzard]

eew old lean 3.4.2

[Kevin Buzzard]

import tactic
import data.finset

variable {α : Type}

def f : nat -> set α := sorry

def fs_up_to (k : ℕ) := (⋃ (i : ℕ) (hi : i ≤ k), f i : set α)

[Eric Wieser]

@Kevin Buzzard, could you elaborate on your 3.4.2 point?

[Kevin Buzzard]

Alistair Tucker linked to the MS version of Lean which hasn't changed for 2 years

[Alistair Tucker]

Yes sorry I need to update my version. Anyway fin is probably not something you need.