# Zulip Chat Archive

## Stream: new members

### Topic: generate_from_le

#### Iocta (Mar 09 2021 at 20:08):

I'm trying to understand the basics of generate_from_le. I don't get what's happening in this step. First of all, what does`m.measurable_set' t`

say, in English?

```
lemma generate_from_le' {s : set (set Ω)} {m : measurable_space Ω}
(h : ∀ t ∈ s, m.measurable_set' t) : generate_from s ≤ m :=
assume t, _
-- don't know how to synthesize placeholder
-- context:
-- Ω : Type,
-- _inst_1 : measurable_space Ω,
-- s : set (set Ω),
-- m : measurable_space Ω,
-- h : ∀ (t : set Ω), t ∈ s → m.measurable_set' t,
-- t : set Ω
-- ⊢ (generate_from s).measurable_set' t ≤ m.measurable_set' t
lemma generate_from_le' {s : set (set Ω)} {m : measurable_space Ω}
(h : ∀ t ∈ s, m.measurable_set' t) : generate_from s ≤ m :=
assume t ht, _
-- don't know how to synthesize placeholder
-- context:
-- Ω : Type,
-- _inst_1 : measurable_space Ω,
-- s : set (set Ω),
-- m : measurable_space Ω,
-- h : ∀ (t : set Ω), t ∈ s → m.measurable_set' t,
-- t : set Ω,
-- ht : (generate_from s).measurable_set' t
-- ⊢ m.measurable_set' t
```

#### Iocta (Mar 09 2021 at 20:12):

First of all, what does`m.measurable_set' t`

say, in English? I think it means `m`

is a sigma algebra and `m.measurable_set' t`

is its set.

#### Iocta (Mar 09 2021 at 20:15):

But then how does adding an argument take "please show the sigma algebra `generate_from s`

's set `t`

is a subset of the sigma algebra `m`

's set -- the same `t`

" to "please show `m`

is a sigma algebra with set `t`

" (if that's what's happening)?

#### Hanting Zhang (Mar 09 2021 at 20:21):

The type of `t`

is `set \Omega`

. `m.measurable_set' t`

means that `t`

is a measurable subset of the space `m`

. `generate_from_le`

is saying that if `s`

is a collection of measurable subsets of `m`

, then the sigma algebra generated by `s`

is less than or equal to the sigma algebra on `m`

.

#### Iocta (Mar 09 2021 at 20:26):

How does adding the `ht`

argument transform the "less than or equal" goal into the `m.measurable_set' t`

goal?

#### Hanting Zhang (Mar 09 2021 at 20:35):

Proving that `(generate_from s).measurable_set' t ≤ m.measurable_set' t`

is defeq to proving that `(generate_from s).measurable_set' t`

implies `m.measurable_set' t`

#### Iocta (Mar 09 2021 at 20:36):

How can I see that?

#### Hanting Zhang (Mar 09 2021 at 20:38):

I think what lean is doing is that its treating `m.measurable_set' t`

as a collection of sets of `\Omega`

, i.e. it has type `set (set \Omega)`

. Then lean looks at the `\le`

symbol and tries to find an instance of a partial order on sets, which exists. Then lean realizes that you're trying to prove that the thing on the left is a subset of the thing on the right.

#### Iocta (Mar 09 2021 at 20:39):

#### Hanting Zhang (Mar 09 2021 at 20:39):

And proving that `a \subset b`

unfolds to `x \in a`

implies `x in b`

.

#### Hanting Zhang (Mar 09 2021 at 20:40):

Well yes, but that's not what you want I think. You're trying to find the partial order that defines what `m₁.measurable_set' ≤ m₂.measurable_set'`

means.

#### Hanting Zhang (Mar 09 2021 at 20:43):

Nevermind, what I've said is inaccurate. I think the gist of what I said is probably the right idea, but it might not be a partial order on sets. It should be directly related to lattices?

#### Hanting Zhang (Mar 09 2021 at 20:45):

You could try going into tactic mode and doing `unfold (\le)`

instead of `intro ht`

and see if it unfolds to a implication

#### Iocta (Mar 09 2021 at 20:48):

```
set_option pp.notation false
lemma generate_from_le' {s : set (set Ω)} {m : measurable_space Ω}
(h : ∀ t ∈ s, m.measurable_set' t) : generate_from s ≤ m :=
begin
intros t,
unfold has_le.le,
unfold preorder.le,
unfold partial_order.le,
unfold semilattice_inf.le,
unfold lattice.le,
unfold linear_order.le,
unfold partial_order.le,
unfold order_bot.le,
unfold bounded_lattice.le,
unfold bounded_distrib_lattice.le,
end
-- 1 goal
-- Ω: Type
-- _inst_1: measurable_space Ω
-- s: set (set Ω)
-- m: measurable_space Ω
-- h: ∀ (t : set Ω), has_mem.mem t s → m.measurable_set' t
-- t: set Ω
-- ⊢ (generate_from s).measurable_set' t → m.measurable_set' t
```

#### Iocta (Mar 10 2021 at 04:06):

What is the tactic version of this?

```
lemma generate_from_le {s : set (set α)} {m : measurable_space α}
(h : ∀ t ∈ s, m.measurable_set' t) : generate_from s ≤ m :=
assume t (ht : generate_measurable s t), ht.rec_on h
(measurable_set_empty m)
(assume s _ hs, measurable_set_compl m s hs)
(assume f _ hf, measurable_set_Union m f hf)
```

I have

```
lemma generate_from_le' {s : set (set Ω)} {m : measurable_space Ω}
(h : ∀ t ∈ s, m.measurable_set' t) : generate_from s ≤ m :=
begin
intros r hr,
cases hr with ha hb t ht he hf ,
{ exact h r hb, },
{ apply measurable_set_empty, },
{
apply measurable_set_compl _ _ _,
sorry,
},
{
sorry,
}
end
```

#### Johan Commelin (Mar 10 2021 at 04:08):

@Iocta you can just fill in the remaining arguments, right?

#### Johan Commelin (Mar 10 2021 at 04:08):

Or otherwise, use `assumption`

, if you want lean to figure them out for you

#### Iocta (Mar 10 2021 at 04:15):

Replacing `sorry`

with `assumption`

doesn't satisfy lean, maybe I don't understand what you mean.

#### Johan Commelin (Mar 10 2021 at 04:20):

What does your goal look like?

#### Johan Commelin (Mar 10 2021 at 04:21):

If you give me something that I can copy-paste into an empty lean file, I can take a look [see #mwe]

#### Iocta (Mar 10 2021 at 04:23):

```
import measure_theory.measure_space
import measure_theory.measurable_space
open measure_theory measure_theory.measure_space classical set
noncomputable theory
variable Ω : Type
variable [measurable_space Ω]
open measurable_space
lemma generate_from_le' {s : set (set Ω)} {m : measurable_space Ω}
(h : ∀ t ∈ s, m.measurable_set' t) : generate_from s ≤ m :=
begin
intros r hr,
cases hr with ha hb t ht he hf ,
{ exact h r hb, },
{ apply measurable_set_empty, },
{
apply measurable_set_compl _ _ _,
sorry,
},
{
sorry,
},
end
```

#### Iocta (Mar 10 2021 at 04:23):

the term version is https://github.com/leanprover-community/mathlib/blob/16ef29135dfe41fba018ef7005909c279bee45f5/src/measure_theory/measurable_space.lean#L302

#### Johan Commelin (Mar 10 2021 at 04:34):

@Iocta the problem was that `cases`

is too crude of a tactic for this job. `induction`

works better:

```
lemma generate_from_le' {s : set (set Ω)} {m : measurable_space Ω}
(h : ∀ t ∈ s, m.measurable_set' t) : generate_from s ≤ m :=
begin
intros t ht,
induction ht with u hu x hx y hy z hz,
{ exact h u hu, },
{ apply measurable_set_empty, },
{ apply measurable_set_compl _ _ _,
assumption, },
{ apply measurable_set_Union,
assumption, },
end
```

#### Iocta (Mar 10 2021 at 05:04):

I see, thanks

#### Iocta (Mar 10 2021 at 20:24):

In measurable_space.lean we have

```
variable [measurable_space α] -- at top level
m : measurable_space α -- in a lemma
```

what is the difference between these two uses of `measurable_space`

?

#### Kevin Buzzard (Mar 11 2021 at 07:42):

You'd use concrete instances when you are reasoning about the collection of all measurable space structures on a type, and type class inference if you just want to fix one measurable space structure once and for all and then do some measure theory.

#### Iocta (Mar 11 2021 at 08:01):

What does it mean that they're both used on the same variable `α`

in that file?

#### Mario Carneiro (Mar 11 2021 at 08:22):

I don't think they are both in scope at the same time

#### Mario Carneiro (Mar 11 2021 at 08:23):

the `[measurable_space A]`

is in a section that ends before the lemma you see

Last updated: May 06 2021 at 22:13 UTC