Indexed families of sets

Stream: new members

[Logan Murphy]

When I declare a family of sets indexed by naturals as in

variable α : Type

variable A : ℕ → set α

does Lean assume that A is an infinite family of sets? If I want to assert that A is a finite family of sets indexed by naturals, can I still use ℕ as the index set or do I have to make some workaround?

[Bryan Gin-ge Chen]

Lean doesn't assume anything about the image of A.

[Logan Murphy]

If I wanted to define a structure where each instance of the structure has an indexed family of n sets , for a particular n, is there a good way to accomplish this? I think the method below works but I'm wondering if I can omit the (i \leq n) somehow.

import data.nat.basic
import data.set.basic
open set nat

variables {α β: Type}

structure ind_fam (α : Type) :=
(n : ℕ)
(A : ∀ (i : ℕ), (i ≤ n) → set α)

[Dan Stanescu]

Take a look at fin n. This may be what you need, but I haven't quite used it before.

structure ind_fam (α : Type) :=
(n : ℕ)
(A : fin (n+1) → set α)

[Kevin Buzzard]

fin (n+1) has size n+1.

[Dan Stanescu]

I thought that was what the initial post meant by (i : ℕ), (i ≤ n), but maybe you mean to say something I don't grasp yet.

[Dan Stanescu]

@Logan Murphy The type fin n is a package made of a value, which is a natural number, together with a proof that the value is strictly less than n. So fin (n+1) is the set {0,1,...,n} because in Lean naturals start at 0.