Zulip Chat Archive

Stream: new members

Topic: Union of k sets


Eric Wieser (Jun 29 2020 at 13:02):

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 (Jun 29 2020 at 13:04):

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

Alistair Tucker (Jun 29 2020 at 13:09):

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

Kevin Buzzard (Jun 29 2020 at 13:52):

eew old lean 3.4.2

Kevin Buzzard (Jun 29 2020 at 13:59):

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 (Jun 29 2020 at 14:04):

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

Kevin Buzzard (Jun 29 2020 at 14:06):

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

Alistair Tucker (Jun 29 2020 at 14:08):

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


Last updated: Dec 20 2023 at 11:08 UTC