Zulip Chat Archive

Stream: new members

Topic: Some questions about working with sets


view this post on Zulip Golol (Oct 19 2020 at 12:40):

I want to define a family of functions f : I -> \a -> \b.
The first question is if it is best to choose I : Type u, or I : set \g, where g : Type u?
What determines if I shoud work with sets and subsets, or types and subtypes?
Now let's say I want to restrict to a smaller set of indices. This means that if f : I -> \b , with I \sub J, then I should be able to create a restriction of f to J.
I have found set.restrict which restricts a function defined on a type to a function defined on a subset of the type, but how can I even define a function on something which is not of type Type u.
Is there a ressource which explains how sets and subsets work and interact?

view this post on Zulip Mario Carneiro (Oct 19 2020 at 12:48):

You should prefer I : Type u

view this post on Zulip Mario Carneiro (Oct 19 2020 at 12:48):

or possibly I : Sort u if possible

view this post on Zulip Mario Carneiro (Oct 19 2020 at 12:49):

Instead of doing restrictions, you should pre-compose with an injection I -> J

view this post on Zulip Mario Carneiro (Oct 19 2020 at 12:49):

these are more generally applicable

view this post on Zulip Yury G. Kudryashov (Oct 19 2020 at 12:51):

Each function in Lean knows its domain: f : α → β has domain α. If you want to restrict it to a subset of the domain, then you either introduce s : set α and use docs#set.restrict, or as @Mario Carneiro suggests pre-compose it with an injection g : γ → α. For the injection, you can either use a bundled docs#function.embedding, or (g : γ → α) (hg : injective g).

view this post on Zulip Yury G. Kudryashov (Oct 19 2020 at 12:52):

Which approach works best for you depends on what exactly do you want to say in Lean.

view this post on Zulip Mario Carneiro (Oct 19 2020 at 12:52):

Generally speaking you will eventually want both forms, but it's easier to get the subset version as a consequence of the type version than the other way around, and the type version also has fewer moving parts so is generally easier to prove too

view this post on Zulip Yury G. Kudryashov (Oct 19 2020 at 12:55):

See also https://leanprover-community.github.io/mathematics_in_lean/sets_functions_and_relations.html

view this post on Zulip Golol (Oct 19 2020 at 13:00):

I think I will go with an injection for now. But this gave me some strange questions about sets.
For example

constant D : set δ
constant b : D

The type of b is uparrow D, so as I understand there is a coercion happening. But in this case could I assume b : δ?

view this post on Zulip Mario Carneiro (Oct 19 2020 at 13:01):

yes, because there is another coercion happening

view this post on Zulip Mario Carneiro (Oct 19 2020 at 13:02):

b : \u D but \u b : delta

view this post on Zulip Yury G. Kudryashov (Oct 19 2020 at 13:09):

b is a pair of (b' : δ) and hb' : b' ∈ D

view this post on Zulip Yury G. Kudryashov (Oct 19 2020 at 13:10):

Lean can coerce it to an element of δ forgetting about hb'.

view this post on Zulip Kevin Buzzard (Oct 19 2020 at 21:25):

If you are using the word "set" as in set theory then this is the wrong way to think about things. S : set alpha means mathematically that S is a subset of alpha, but S is not a type, it's a term, and functions go from types to types, so you should stick to types if you can and then you can avoid the coercions

view this post on Zulip Kevin Buzzard (Oct 19 2020 at 21:27):

If you want an S representing a subset of alpha and you want to think of it as a type then you could use a subtype. But depending on what you're doing, "categorifying" and considering injections from other types rather than subsets or subtypes might be the easiest thing to do

view this post on Zulip Kevin Buzzard (Oct 19 2020 at 21:30):

Note that distinct types are disjoint by definition, so when translating informal mathematics into type theory one sometimes has to think a little to figure out how to express things (in the sense that as someone who was brought up with ZFC I had to learn some tricks)

view this post on Zulip Kevin Buzzard (Oct 19 2020 at 21:30):

In particular I \subset J doesn't make sense for types

view this post on Zulip Golol (Oct 19 2020 at 23:31):

I have a silly question... I have ht : t \in {b : set \a : P b}. How do I get h : P from this?

view this post on Zulip Kevin Buzzard (Oct 19 2020 at 23:32):

what is the type of everything? Can you post fully working code?

view this post on Zulip Kevin Buzzard (Oct 19 2020 at 23:33):

{b : set \a : P b} makes no sense to me

view this post on Zulip Kevin Buzzard (Oct 19 2020 at 23:33):

and neither does h : P

view this post on Zulip Golol (Oct 19 2020 at 23:33):

So the exact hypothesis would be
ht: t ∈ {B : set (I → β) | ∃ (A : set β) (ha : m.is_measurable' A) (i : I), B = cylinder I m A ha i}.
Sorry, the way I wrote it wasn't correct, I used : instead of |

view this post on Zulip Golol (Oct 19 2020 at 23:34):

and I want h : ∃ (A : set β) (ha : m.is_measurable' A) (i : I), t = cylinder I m A ha i

view this post on Zulip Kevin Buzzard (Oct 19 2020 at 23:35):

that's equal to ht by definition

view this post on Zulip Kevin Buzzard (Oct 19 2020 at 23:35):

you can just do cases on ht

view this post on Zulip Golol (Oct 19 2020 at 23:35):

ah hmmm

view this post on Zulip Kevin Buzzard (Oct 19 2020 at 23:36):

t \in {a : X | P a} is just syntax sugar for P t

view this post on Zulip Golol (Oct 19 2020 at 23:39):

ah very nice, thanks. I knew it had to be something trivial.

view this post on Zulip Golol (Oct 20 2020 at 00:48):

We have a partial order on measurable spaces, where m \le n basically stands for m.measurable' \le n.measurable'. I see the field .le in the constructor of the partial order but I don't know how to use it for hle.

hex_h: (measurable_space.comap (λ (f : I  β), f i) m).is_measurable' t
hle: (λ (j : I), measurable_space.comap (λ (f : I  β), f j)) i   (j : I), measurable_space.comap (λ (f : I  β), f j)
 ( (i : I), measurable_space.comap (λ (f : I  β), f i) m).is_measurable' t

view this post on Zulip Mario Carneiro (Oct 20 2020 at 01:30):

I don't understand your question. But hle unfolds to a forall statement about sets being measurable, so most likely have := hle t should show you more information about what the real type of that thing is

view this post on Zulip Mario Carneiro (Oct 20 2020 at 01:31):

Something seems off about hle though, because the lhs is missing an m, that is actually an inequality of functions

view this post on Zulip Golol (Oct 20 2020 at 07:49):

I was tired when I typed it yesterday, a better description of the situation should the following:

m n : measurable_space \b
t : set \b
hex_h : m.is_measurable' t
hle : m \le n
(although it is technically more like hle : ( \lambda i, m) i \le m)
|- n.is_measurable' t

view this post on Zulip Mario Carneiro (Oct 20 2020 at 08:05):

it's generally better to make a targeted #mwe than sketch a tactic state

view this post on Zulip Golol (Oct 20 2020 at 08:12):

Yes you're right sorry, I should'Ve put more thought into this one because I just realized I was basically missing a character :grinning:

view this post on Zulip Kevin Buzzard (Oct 20 2020 at 08:32):

Making the MWE is a very good way to put that kind of thought in.


Last updated: May 09 2021 at 18:17 UTC