Declaration

Stream: new members

[Alex Zhang]

variables n: ℕ
variables {p : Type*} [fintype p]
variables {α_set :Type*} [finset α_set]

declares that p is a finite type and α_set is a finite set.
How can I declare a finite type and a finite set of cardinal n for both?

[Kevin Buzzard]

No, finset is not a class, the code you wrote about finsets does not make sense (although it probably parses)

[Kevin Buzzard]

What you have written is "let alpha_set be a type and let _inst_2 (or whatever lean called it because you didn't give it a name) be a finite subset of alpha_set. And then lean attempts to put this finite set into the type class system which will then ignore it because finset isn't a class

[Kevin Buzzard]

There are no such thing as sets in type theory, there are only subsets of a type. At least that's my mental model of sets in Lean

[Kevin Buzzard]

If you want to say that p has size n you can just ask that fintype.card p = n

[Alex Zhang]

Yes, the third line of my code is problematic, I will fix it., although this is not the problem I am concerned here.

[Kevin Buzzard]

Once you've fixed it the answer is probably docs#finset.card

[Kevin Buzzard]

Although if you are not interested in constructivism then I might be able to interest you in nat.card which takes the size of pretty much anything and returns a natural, which is 0 if the input is infinite (rather like 1/X returning 0 if X=0)

[Alex Zhang]

Kevin Buzzard said:

If you want to say that p has size n you can just ask that fintype.card p = n

I don't quite understand how to do this. Could you please give me a full code?

[Kevin Buzzard]

I'm afraid I'm on my phone. What happens if you just add that as a hypothesis?

[Kevin Buzzard]

It's the first time I've been out the house in months -- I'm just coming back from my second Covid jab!

[Alex Zhang]

It is easy to add it as a hypothesis, but what I really want to do is to construct/declare a fintype or finset of cardinal n instead of giving that as a hypothesis.

[Kevin Buzzard]

I don't understand the difference

[Johan Commelin]

Maybe Alex wants a bundled "finset-of-cardinality-n"

[Johan Commelin]

variables (s : {x : finset X // x.card = n})

[Alex Zhang]

Johan Commelin said:

Maybe Alex wants a bundled "finset-of-cardinality-n"

Exactly

[Kevin Buzzard]

But mathematically this is exactly the same data

[Kevin Buzzard]

You can package it up like Johan suggests but at the end of the day you'll just unpack it again :-)

[Johan Commelin]

@Alex Zhang My guess is that you'll find the unbundled approach easier to work with in Lean

[Alex Zhang]

Johan Commelin said:

Alex Zhang My guess is that you'll find the unbundled approach easier to work with in Lean

uhmm, how do you exactly do this?

[Johan Commelin]

Just follow Kevin's advice, and add the hypothesis

[Johan Commelin]

example (s : {x : finset X // x.card = n}) : true :=
-- vs
example (s : finset X) (hs : s.card = n) : true :=

[Alex Zhang]

Am I able to declare p to be a fintype of cardinal n after variables {p q : Type*} or variables before any statement of an example or a theorem?

[Kevin Buzzard]

Bundling and unbundling are words which are used to express how lean stores mathematical ideas. For example, for a group homomorphism $G\to H$ you could either store it "unbundled" as two things, a function f : G → H and a proof hf : ∀ a b, f(a*b)=f(a)*f(b) or "bundled" as f : G →* H where f is now one object, a term of a structure which contains both the map and the proof all in one. Whether you should bundle a mathematical idea or not is a delicate question and not a mathematical one!

[Kevin Buzzard]

We're suggesting that to store a finite type of size n you're better off with the unbundled approach, so you will have a term without a name of type fintype p and which will be dealt with by the typeclass system, and then a hypothesis hp : card p = n which you'll carry around. You don't need to bundle because the type class inference system will handle the finiteness statements for you.

[Alex Zhang]

Alex Zhang said:

Am I able to declare p to be a fintype of cardinal n after variables {p q : Type*} or variables before any statement of an example or a theorem?

I am still curious about this question.

[Kevin Buzzard]

I don't understand the question

[Kevin Buzzard]

Just add the hypotheses you want where you want them? Is that the answer?

[Alex Zhang]

Yeah, I understand your suggestion.