# Zulip Chat Archive

## Stream: new members

### Topic: Some questions about working with sets

#### 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?

#### Mario Carneiro (Oct 19 2020 at 12:48):

You should prefer `I : Type u`

#### Mario Carneiro (Oct 19 2020 at 12:48):

or possibly `I : Sort u`

if possible

#### Mario Carneiro (Oct 19 2020 at 12:49):

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

#### Mario Carneiro (Oct 19 2020 at 12:49):

these are more generally applicable

#### 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)`

.

#### 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.

#### 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

#### Yury G. Kudryashov (Oct 19 2020 at 12:55):

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

#### 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 : δ?

#### Mario Carneiro (Oct 19 2020 at 13:01):

yes, because there is another coercion happening

#### Mario Carneiro (Oct 19 2020 at 13:02):

`b : \u D`

but `\u b : delta`

#### Yury G. Kudryashov (Oct 19 2020 at 13:09):

`b`

is a pair of `(b' : δ)`

and `hb' : b' ∈ D`

#### Yury G. Kudryashov (Oct 19 2020 at 13:10):

Lean can coerce it to an element of `δ`

forgetting about `hb'`

.

#### 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

#### 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

#### 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)

#### Kevin Buzzard (Oct 19 2020 at 21:30):

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

#### 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?

#### Kevin Buzzard (Oct 19 2020 at 23:32):

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

#### Kevin Buzzard (Oct 19 2020 at 23:33):

`{b : set \a : P b}`

makes no sense to me

#### Kevin Buzzard (Oct 19 2020 at 23:33):

and neither does `h : P`

#### 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 |

#### 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`

#### Kevin Buzzard (Oct 19 2020 at 23:35):

that's equal to `ht`

by definition

#### Kevin Buzzard (Oct 19 2020 at 23:35):

you can just do cases on ht

#### Golol (Oct 19 2020 at 23:35):

ah hmmm

#### Kevin Buzzard (Oct 19 2020 at 23:36):

`t \in {a : X | P a}`

is just syntax sugar for `P t`

#### Golol (Oct 19 2020 at 23:39):

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

#### 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
```

#### 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

#### 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

#### 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
```

#### Mario Carneiro (Oct 20 2020 at 08:05):

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

#### 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:

#### 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