# Zulip Chat Archive

## Stream: new members

### Topic: lemmas and structs

#### Iocta (Mar 08 2021 at 07:22):

What is the relationship between `measurable_space.measurable_set_compl`

and `measurable_set.compl`

? https://github.com/leanprover-community/mathlib/blob/16ef29135dfe41fba018ef7005909c279bee45f5/src/measure_theory/measurable_space.lean#L78-L98

#### Iocta (Mar 08 2021 at 07:29):

e.g. why can't I use this comment instead of the code it follows?

```
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 Ω]
example [encodable I] (f : I → set Ω) (h : ∀ i : I, measurable_set (f i)) : measurable_set (⋂ i, f i) :=
begin
apply measurable_set.compl_iff.1,
rw compl_Inter,
apply measurable_set.Union, -- apply ‹measurable_space Ω›.measurable_set_Union,
intro i,
apply measurable_set.compl_iff.2,
exact h i,
end
```

#### Kevin Buzzard (Mar 08 2021 at 08:27):

I don't know this part of the library at all but it seems to me that the answer to why the commented `apply`

doesn't work is simply that the two functions are different, the one that works wants a function from an encodable set (which you have) and the one that doesn't work wants a function from nat (which you don't have). you say "e.g." but it seems to me that this question is different from the question in your first post, the answer to which is probably just that the rephrasing makes it possible to use dot notation because it puts it in the `measurable_set`

namespace so now if `hs`

is a proof that `s`

is measurable then `hs.compl`

is a proof that its complement is measurable. See for example the proof of `measurable_set.Inter`

.

Last updated: May 15 2021 at 23:13 UTC