## Stream: new members

### Topic: measurable_space

#### Iocta (Aug 13 2020 at 21:40):

What is going on here?

import analysis.normed_space.indicator_function
import measure_theory.set_integral
import analysis.specific_limits
import data.real.basic
import data.nat.basic
import algebra.geom_sum

open set filter topological_space measure_theory

section e2_7_1

@[derive decidable_eq]
inductive letter : Type
| a : letter
| b : letter
| c : letter
| d : letter

namespace letter

instance fintype: fintype letter :=
{elems := {a, b, c, d}, complete := λ x, by cases x; simp}

def f1 : set (set letter) := {{}, {a, b}, {c, d}, {a,b,c,d}}

-- from mathlib:
-- /-- A measurable space is a space equipped with a σ-algebra. -/
-- structure measurable_space (α : Type u) :=
-- (is_measurable : set α → Prop)
-- (is_measurable_empty : is_measurable ∅)
-- (is_measurable_compl : ∀s, is_measurable s → is_measurable sᶜ)
-- (is_measurable_Union : ∀f:ℕ → set α, (∀i, is_measurable (f i)) → is_measurable (⋃i, f i))

example : measurable_space f1 :=
begin
split,
{  exact rfl, },
{
intros s h,
-- s: set ↥f1
-- h: ∅ = s
-- ⊢ ∅ = sᶜ
},
{ sorry },
{ sorry }
end

end letter

end e2_7_1


#### Iocta (Aug 13 2020 at 21:43):

Is it asking me to show that the complement of {} in {{}, {a, b}, {c, d}, {a,b,c,d}} is {}? I don't think that's true.

#### Reid Barton (Aug 13 2020 at 21:43):

You have gone wrong starting with measurable_space f1

#### Iocta (Aug 13 2020 at 21:44):

Oh. What do I mean?

#### Reid Barton (Aug 13 2020 at 21:45):

Also, I would recommend using fsplit rather than split--that will present the subgoals in the order you expect

#### Reid Barton (Aug 13 2020 at 21:47):

Try using fsplit instead of split, and then pay close attention to what Lean is asking for

#### Reid Barton (Aug 13 2020 at 21:47):

And look at the definition of measurable_space again.

#### Iocta (Aug 13 2020 at 21:54):

well I can finish the proof but as you said, I'm pretty sure this is not what I meant :-D

example : measurable_space f1 :=
begin
fsplit,
{
exact (λs, true),
},
{
exact trivial,
},
{
intros a b,
trivial,
},
{
intros a b,
trivial,
},
end


#### Iocta (Aug 13 2020 at 23:25):

So maybe what I mean is example : measurable_space letter :=, but then the first step is ⊢ set letter -> Prop, and I can start by saying

intro s, have s_finite: finite s, exact finite.of_fintype s,


which leaves ⊢ Prop and I'd say something involving finset.is_measurable....?

#### Kevin Buzzard (Aug 13 2020 at 23:25):

If you have ⊢ Prop you're doing something very wrong, although you could solve it using Fermat's Last Theorem

haha okay

#### Kevin Buzzard (Aug 13 2020 at 23:26):

Did you look at the type of measurable_space yet? I have never used it but my impression is that if it's data then you shouldn't be anywhere near a begin/end block

#### Iocta (Aug 13 2020 at 23:26):

yeah I quoted it in the first paste

#### Kevin Buzzard (Aug 13 2020 at 23:26):

You make structures in Lean with the { foo := bar, baz := moo } constructor usually

#### Kevin Buzzard (Aug 13 2020 at 23:27):

Oh Ok great thanks: then you should write example : measurable_space f1 := _ and then click on the light bulb and then click on the last but one option about fields of a structure and then go ahead and fill those in

#### Kevin Buzzard (Aug 13 2020 at 23:28):

this is assuming you want to put a measurable space structure on f1

#### Kevin Buzzard (Aug 13 2020 at 23:28):

which to be frank looks highly unlikely

#### Iocta (Aug 13 2020 at 23:32):

I think what I'm trying to say is f1 has {}, is closed under complement, and countable union/intersection

#### Iocta (Aug 13 2020 at 23:33):

which is at least similar to the generated

example : measurable_space XXXX := {
is_measurable := _,
is_measurable_empty := _,
is_measurable_compl := _,
is_measurable_Union := _ }


for some XXXX

#### Iocta (Aug 13 2020 at 23:35):

but you both say I don't mean measurable_space f1, so I'm not sure what I do mean

#### Iocta (Aug 13 2020 at 23:38):

maybe i mean

example : measurable_space letter := {
is_measurable := (λ s, s ∈ f1),
is_measurable_empty := _,
is_measurable_compl := _,
is_measurable_Union := _ }


i'll try that

#### Iocta (Aug 14 2020 at 00:28):

⊢ ∅ ∈ f1 woulda thought rfl would work, but no dice

#### Iocta (Aug 14 2020 at 00:40):

Since def f1 : set (set letter) := {{}, {a, b}, {c, d}, {a,b,c,d}}, shouldn't it follow immediately that {} \in f1?

#### Alex J. Best (Aug 14 2020 at 00:41):

Well just because its obvious to you do doesn't mean its trivial!

#### Alex J. Best (Aug 14 2020 at 00:42):

The notation {{}, {a,b}, {c,d}, {a,b,c,d}} means something. Try adding set_option pp.notation false above your example to turn notation off, and you'll see it is really a sequence of elements inserted into a singleton set.

#### Alex J. Best (Aug 14 2020 at 00:43):

So probably there is a sequence of lemmas that do it, or maybe a tactic like finish.

#### Alex J. Best (Aug 14 2020 at 00:47):

First thing is to rw f1 though if you didn't already.

#### Alex J. Best (Aug 14 2020 at 00:48):

In this case it is in fact a single lemma after you've done that

#### Iocta (Aug 14 2020 at 00:52):

Ok that works.

Last updated: May 10 2021 at 00:31 UTC