Some questions about working with sets

Stream: new members

[Golol]

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]

You should prefer I : Type u

[Mario Carneiro]

or possibly I : Sort u if possible

[Mario Carneiro]

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

[Mario Carneiro]

these are more generally applicable

[Yury G. Kudryashov]

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]

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

[Mario Carneiro]

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]

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

[Golol]

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]

yes, because there is another coercion happening

[Mario Carneiro]

b : \u D but \u b : delta

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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]

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]

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]

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

[Golol]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and neither does h : P

[Golol]

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]

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

[Kevin Buzzard]

that's equal to ht by definition

[Kevin Buzzard]

you can just do cases on ht

[Golol]

ah hmmm

[Kevin Buzzard]

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

[Golol]

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

[Golol]

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]

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]

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

[Golol]

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]

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

[Golol]

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]

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