measurable_space

Stream: new members

[Iocta]

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]

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]

You have gone wrong starting with measurable_space f1

[Iocta]

Oh. What do I mean?

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

And look at the definition of measurable_space again.

[Iocta]

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]

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]

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

[Iocta]

haha okay

[Kevin Buzzard]

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]

yeah I quoted it in the first paste

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

which to be frank looks highly unlikely

[Iocta]

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

[Iocta]

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]

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

[Iocta]

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]

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

[Iocta]

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]

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

[Alex J. Best]

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]

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

[Alex J. Best]

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

[Alex J. Best]

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

[Iocta]

Ok that works.