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

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

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