semialgebra setminus

Stream: new members

[Iocta]

What's wrong here?

import data.finset.basic

open set

variables {α : Type*}

structure semialgebra (α : Type*) :=
(semialgebra' : set (set α) → Prop)
(semialgebra_empty : semialgebra' ∅)
(semialgebra_inter : ∀ (s : set (set α)) (hs : semialgebra' s) (s1 s2 : set α), s1 ∈ s → s2 ∈ s → (s1 ∩ s2) ∈ s)
(semialgebra_difference : ∀ (s t : set (set α)), ∃ c : finset (set α), (finset.bUnion c) = s \ t)

-- type mismatch at application
--   has_sdiff.sdiff s
-- term
--   s
-- has type
--   set (set α) : Type ?
-- but is expected to have type
--   (set α → finset ?m_1) → finset ?m_1 : Type (max ? ?)

[Alex J. Best]

I think your definition has too many levels of nested sets, set X is the power set set (set X) is subsets of the power set but set (set X)) \to Prop is another condition on those, so a further power set.

import data.finset.basic

open set


structure semialgebra (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_difference : ∀ (s t : set α), in_semialgebra s → in_semialgebra t → ∃ c : finset (set α), ∀ s' ∈ c, in_semialgebra s' → (sUnion (c : set (set α))) = s \ t)

looks more like what I read on https://en.wikibooks.org/wiki/Measure_Theory/Basic_Structures_And_Definitions/Semialgebras,_Algebras_and_%CF%83-algebras if that's what youre trying.

[Alex J. Best]

I had to cast the finset to a set to take the set docs#set.sUnion and also deleted the repeated introduction of alpha.

[Alex J. Best]

I guess that page also includes a pairwise disjoint condition which is missing from what I wrote

[Iocta]

I see. That in_ naming scheme is very clarifying. I was confused thinking the first component's argument was the semialgebra instead of a member of it.

[Iocta]

image.png

is the "disjoint" condition actually doing any work or can I just delete it?

[Iocta]

import data.finset.basic

open set

variables {α : Type*}

structure semialgebra' (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), sUnion (c : set (set α)) = sᶜ)

[Iocta]

(Also, why is that definition so different from the one on wikibooks)

[Iocta]

I thought it was gonna ask me to show that empty is in I, but it's asking for nullset equals I. I guess I've made the same mistake again, but I don't see how.

import measure_theory.measure_space

open measure_theory measure_theory.measure_space classical set

structure semialgebra (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), sUnion (c : set (set α)) = sᶜ)

example (I : {s : set ℝ // ∃ (a b : ℝ), s = Icc a b}) : semialgebra I := {
  in_semialgebra := heq I,
  semialgebra_empty := _,
  semialgebra_inter := _,
  semialgebra_compl := _
}

-- don't know how to synthesize placeholder
-- context:
-- I : {s // ∃ (a b : ℝ), s = Icc a b}
-- ⊢ I == ∅

[Eric Wieser]

Are you sure you want heq I as your in_semi_algebra?

[Eric Wieser]

It's very rare to want docs#heq unless you're really running into dependently-typed trouble

[Eric Wieser]

Is it possible you wanted this?

example : semialgebra ℝ := {
  -- the semialgebra contains closed intervals of ℝ
  in_semialgebra := λ s, ∃ (a b : ℝ), s = Icc a b,
  semialgebra_empty := ⟨0, 0, sorry⟩,
  semialgebra_inter := sorry,
  semialgebra_compl := sorry
}

[Iocta]

That looks more right, I'll try that

[Iocta]

I guess that's actually asking me to show $[0,0] = \emptyset$ which probably isn't true. So maybe my statement of the problem is broken in the first place.

[Eric Wieser]

Oh yeah, I forgot what closed meant!

[Iocta]

What is this error?

import measure_theory.measure_space

open measure_theory measure_theory.measure_space classical set

structure semialgebra (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), sUnion (c : set (set α)) = sᶜ)


example : semialgebra ℝ := {
  in_semialgebra := λ s, s = ∅ ∨ ∃ (a b : ℝ),  (a < b → s = (Ioc a b)),
  semialgebra_empty := or.inl rfl,
  semialgebra_inter := begin
    intros s1 s2 h1 h2,
    cases h1 with h1 h1,
    {
      cases h2 with h2 h2,
      {
        left,
        rw [h1, empty_inter],
      },
      {
        left,
        rw [h1, empty_inter],
      },
    },
    {
      cases h2,
      {
        left,
        rw [h2, inter_empty],
      },
      {
        right,
        cases h1 with a1 h1,
        cases h1 with b1 h1,
        rw h1,
        cases h2 with a2 h2,
        cases h2 with b2 h2,
        rw h2,
        {
          use a1 ⊔ a2,
          use b1 ⊓ b2,
          intro h,
          rw Ioc_inter_Ioc,
        },
        {
          apply (classical.em (a2 < b2)),
          -- invalid apply tactic, failed to unify
          --   a2 < b2
          -- with
          --   a2 < b2 ∨ ¬a2 < b2
          -- state:
          -- s1 s2 : set ℝ,
          -- a1 b1 : ℝ,
          -- h1 : a1 < b1 → s1 = Ioc a1 b1,
          -- a2 b2 : ℝ,
          -- h2 : a2 < b2 → s2 = Ioc a2 b2
          -- ⊢ a2 < b2
        },
        {
          sorry,
        },
      },
    }
  end,
  semialgebra_compl := begin
    sorry
  end
}

[Kevin Buzzard]

Do you understand what the apply tactic does? It changes a goal of the form Q to a goal of the form P if you apply f : P -> Q.

[Kevin Buzzard]

Where is your function of the form P -> Q which you're applying?

[Iocta]

It's in h2

[Kevin Buzzard]

if h2 is of the form P -> Q then you should apply h2 instead, and it will work as long as your goal is Q. You are applying a theorem of the form "P or Q is true" and this isn't a function so you can't apply it.

[Iocta]

Er that's not right. h2 is P -> Q and I have P in goal. I think I should be able to say P is either true or it isn't. In case it's true, that's sufficient; in case it isn't I'm gonna try to find a contradiction.

[Kevin Buzzard]

Sure you can do that but apply doesn't do that. Maybe you want the by_cases tactic?

[Kevin Buzzard]

Oh if P is your goal then maybe by_contra is a quicker way to get where you want to go

[Kevin Buzzard]

Aah -- you use cases to split P or Q into a P line and a Q line so maybe another approach is to just change your apply to a cases. But by_contra will get you there more quickly.

[Eric Wieser]

That goal looks untrue to me

[Kevin Buzzard]

∃ (a b : ℝ), (a < b → s = (Ioc a b)) should surely be "a < b and s = ...". Otherwise such a and b always exist, just take a=1 and b=0.

[Iocta]

Like this? in_semialgebra := λ s, s = ∅ ∨ ∀ (a b : ℝ), (a < b ∧ s = (Ioc a b)),

[Kevin Buzzard]

That looks right, but why not just drop a < b and the s = emptyset as well, because when a>=b Ioc a b is just the empty set anyway.

[Iocta]

Oh that's much nicer

[Kevin Buzzard]

It's crazy how these things sometimes come out really super-nicely sometimes.

[Iocta]

I think I missed something. If the statement is just in_semialgebra := λ s, ∀ (a b : ℝ), s = (Ioc a b), then semialgebra_empty will ask me to show that forall a b, Ioc a b = emptyset, which doesn't seem true.

[Kevin Buzzard]

There's something wrong with compl as well. Right now you can just let c = {s^compl}. If you restrict to all the elements of c being in your semialgebra then you can't make the complement of [0,1) because every set in your semialgebra has finite measure and so a finite union will do too. I think you might need the infinity versions of Ioc. I've forgotten what they're called though.

[Iocta]

Iic?

[Kevin Buzzard]

yes it could well be that

[Kevin Buzzard]

docs#set.Iic

[Kevin Buzzard]

Yes, that. But I don't want to tell you what your semialgebra is -- it's your definition.

[Iocta]

I'm trying to copy image.png

[Iocta]

But one dimensional for now

[Kevin Buzzard]

note the possibility that a and b can be infinity.

[Iocta]

Well I guess I was sorta mixing that with image.png from https://en.wikibooks.org/wiki/Measure_Theory/Basic_Structures_And_Definitions/Semialgebras,_Algebras_and_%CF%83-algebras

[Iocta]

But maybe those definitions are actually not talking about the same object

[Iocta]

(deleted)

[Iocta]

Yeah this can't be right

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

structure semialgebra (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), sUnion (c : set (set α)) = sᶜ)


example : semialgebra ereal := {
  in_semialgebra := λ s, ∀ (a b : ereal), s = (Ioc a b),
  semialgebra_empty := begin
      intros a b,
  -- a b: ereal
  -- ⊢ ∅ = Ioc a b
  end,
  semialgebra_inter := begin
    sorry,
  end,
  semialgebra_compl := begin
    sorry
  end
}

[Iocta]

Gotta be

example : semialgebra ereal := {
  in_semialgebra := λ s, ∃ (a b : ereal), s = (Ioc a b),
  semialgebra_empty := ⟨0, 0, sorry⟩,
  semialgebra_inter := begin
    sorry,
  end,
  semialgebra_compl := begin
    sorry
  end

[Eric Wieser]

Isn't that what I posted earlier?

[Eric Wieser]

Ah, Ioc instead of Icc

[Iocta]

It's very close, also changed real to ereal

[Iocta]

I'm trying to make a finset with this these two elements but Lean doesn't know how to put the elements in the finset.

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

structure semialgebra (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), sUnion (c : set (set α)) = sᶜ)

example : semialgebra ereal := {
  in_semialgebra := λ s, ∃ (a b : ereal), s = (Ioc a b),
  semialgebra_empty := ⟨0, 0, sorry⟩,
  semialgebra_inter := begin
    intros s1 s2 h1 h2,
    cases h1 with a1 ha1,
    {
      cases ha1 with b1 hb1,
      {
        cases h2 with a2 ha2,
        {
          cases ha2 with b2 hb2,
          use a1 ⊔ a2,
          use b1 ⊓ b2,
          rw [hb1, hb2, Ioc_inter_Ioc],
        },
      },
    },
  end,
  semialgebra_compl := begin
    intros s hs,
    cases hs with a h,
    cases h with b h,
    rw h,
    have t : finset (set ereal) := {(Iic a) , (Ioi b)},
-- failed to synthesize type class instance for
-- s : set ereal,
-- a b : ereal,
-- h : s = Ioc a b
-- ⊢ has_insert ?m_1 (finset (set ereal))
-- state:
-- s : set ereal,
-- a b : ereal,
-- h : s = Ioc a b
-- ⊢ ∃ (c : finset (set ereal)), ⋃₀↑c = (Ioc a b)ᶜ
  end
}

[Scott Morrison]

Are you just missing decidable instances? What happens if you open_locale classical, or use classical at the beginning of the proof?

[Iocta]

Yeah that was it

[Iocta]

How can I solve this?

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

open_locale classical

lemma compl_Ioc (a b : ereal) : (Ioc a b)ᶜ  = Iic a ∪ Ioi b :=
begin
  sorry,
end

[Iocta]

I think it's true

[Johan Commelin]

Does ext get you started?

[Eric Wieser]

rw [mem_union_eq, mem_Ioi, mem_Iic, mem_compl_eq, mem_Ioc] will then get you most of the way to finished

[Eric Wieser]

I think it might be worth PRing that lemma, once golfed to:

lemma compl_Ioc (a b : ereal) : (Ioc a b)ᶜ = Iic a ∪ Ioi b :=
set.ext $ λ _, not_and_distrib.trans (or_congr not_lt not_le)

[Eric Wieser]

Along with the other three variants of o and c

[Iocta]

This works now. How can I make it shorter?

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

open_locale classical

structure semialgebra (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), sUnion (c : set (set α)) = sᶜ)


lemma compl_Ioc (a b : ereal) : (Ioc a b)ᶜ = Iic a ∪ Ioi b :=
set.ext $ λ _, not_and_distrib.trans (or_congr not_lt not_le)


example : semialgebra ereal := {
  in_semialgebra := λ s, ∃ (a b : ereal), s = (Ioc a b),
  semialgebra_empty := ⟨0, 0, by simp only [mem_empty_eq, forall_const, not_false_iff, Ioc_self],⟩,
  semialgebra_inter := begin
    intros s1 s2 h1 h2,
    cases h1 with a1 ha1,
    {
      cases ha1 with b1 hb1,
      {
        cases h2 with a2 ha2,
        {
          cases ha2 with b2 hb2,
          use a1 ⊔ a2,
          use b1 ⊓ b2,
          rw [hb1, hb2, Ioc_inter_Ioc],
        },
      },
    },
  end,
  semialgebra_compl := begin
    intros s hs,
    cases hs with a h,
    cases h with b h,
    rw h,
    let t : finset (set ereal) := {(Iic a) , (Ioi b)},
    use t,
    have: ⋃₀↑t =  (Iic a) ∪ (Ioi b),
    from by simp only [finset.coe_insert, sUnion_singleton, finset.coe_singleton, sUnion_insert],
    rw [this],
    rw [compl_Ioc],
  end
}

[Eric Wieser]

Yours intros and four cases tactics can be combined into a single rintros

[Eric Wieser]

rintros s1 s2 ⟨a1, b1, rfl⟩ ⟨a2, b2, rfl⟩

[Eric Wieser]

Here's how I'd golf the whole thing:

example : semialgebra ereal := {
  in_semialgebra := λ s, ∃ (a b : ereal), s = Ioc a b,
  semialgebra_empty := ⟨0, 0, (Ioc_self _).symm⟩,
  semialgebra_inter := begin
    rintros s1 s2 ⟨a1, b1, rfl⟩ ⟨a2, b2, rfl⟩,
    exact ⟨a1 ⊔ a2, b1 ⊓ b2, Ioc_inter_Ioc⟩,
  end,
  semialgebra_compl := begin
    rintros s ⟨a, b, rfl⟩,
    refine ⟨{Iic a, Ioi b}, eq.trans _ (compl_Ioc _ _).symm⟩,
    simp only [finset.coe_insert, sUnion_singleton, finset.coe_singleton, sUnion_insert],
  end }

[Iocta]

rintros s1 s2 ⟨a1, b1, rfl⟩ ⟨a2, b2, rfl⟩, works but if I replace it with rintros s1 s2 ⟨a1, b1, _⟩ ⟨a2, b2, _⟩, then it doesn't work. What is the difference?

[Eric Wieser]

rfl is like introducing h then immediately doing rw h

[Eric Wieser]

Although that's a bit of a simplification

[Iocta]

Whereas the _ is just introducing h?

[Iocta]

rintros s1 s2 ⟨a1, b1, h1⟩ ⟨a2, b2, h2⟩,
rw [h1, h2],

does work

[Eric Wieser]

Yeah, _ just tells lean to pick a name for you

[Iocta]

This works, what does a shorter version look like?

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

open_locale classical
noncomputable theory


structure algebra' (α : Type*) :=
(in_algebra : set α → Prop)
(algebra_empty : in_algebra ∅)
(algebra_compl : ∀ (s : set α), in_algebra s → in_algebra sᶜ)
(algebra_union : ∀ (s1 s2 : set α), in_algebra s1 → in_algebra s2 → in_algebra (s1 ∪ s2))


lemma eq_compl_of_compl_eq (s1 s2: set ℤ) (h : s1ᶜ = s2) : s1 = s2ᶜ :=
begin
ext,
split;
{
  intro h,
  simp only [mem_compl_eq] at *,
  finish,
},
end


example : algebra' ℤ := {
  in_algebra := λs, ∃ (t : finset ℤ), (s = t) ∨ (sᶜ = t),
  algebra_empty :=
  ⟨finset.empty, or.inl rfl⟩,
  algebra_compl := begin
    intros s hs,
    cases hs with t ht,
    cases ht with h ht,
    {
      use t,
      rw [compl_compl],
      right,
      exact h,
    },
    {
      use t,
      left,
      exact ht,
    }
  end,
  algebra_union := begin
    rintros s1 s2 ⟨t1, h1⟩ ⟨t2, h2⟩,
    cases h1,
    {
      cases h2,
      {
        use t1 ∪ t2,
        left,
        simp only [finset.coe_union],
        simp only [*],
      },
      {
        use t2.filter (λx, x ∉ s1),
        right,
        rw [compl_union],
        ext,
        simp only [mem_sep_eq, mem_inter_eq, finset.mem_coe, mem_compl_eq, finset.coe_filter],
        split,
        simp only [*, and_imp, finset.mem_coe] at *,
        {
          intros h h',
          split,
          {
            have: s2 = t2ᶜ,
            from by {
              apply eq_compl_of_compl_eq,
              exact h2,
            },
            simp only [*, not_not, finset.mem_coe, mem_compl_eq] at *,
          },
          { exact h, },
        },
        {
          intros h,
          split,
          { exact h.2,  },
          {
            cases h,
            rw [←mem_compl_eq],
            simp only [*, finset.mem_coe] at *,
          },
        },
      },
    },
    {
      cases h2,
      {
        use t1.filter (λx, x ∉ s2),
        right,
        rw [compl_union],
        ext,
        split,
        {
          intro h,
          simp only [*, mem_sep_eq, mem_inter_eq, not_false_iff, and_self, mem_compl_eq, finset.coe_filter] at *,
        },
        {
          intro h,
          have: s1 = t1ᶜ,
          from by {
            apply eq_compl_of_compl_eq,
            exact h1,
          },
          {
            simp only [*, mem_sep_eq, mem_inter_eq, not_false_iff, and_self, mem_compl_eq, finset.coe_filter] at *,
          },
        },
      },
      {
        use t1.filter (λx, x ∈ t2),
        have h1': s1 = t1ᶜ,
        from by {
          apply eq_compl_of_compl_eq,
          exact h1,
        },
        have: s2 = t2ᶜ,
        from by {
          apply eq_compl_of_compl_eq,
          exact h2,
        },
        right,
        ext,
        simp only [*, mem_sep_eq, compl_union, mem_inter_eq, iff_self, finset.mem_coe, finset.coe_filter] at *,
      },
    },
  end
}

[Kevin Buzzard]

"have, from by apply exact" can all be done in one line, and one has to question whether it's even necessary given that you're about to close the goal with a simp * -- just throw the proof directly into the list of things in the list

[Kevin Buzzard]

intros, cases can be done with rintro

[Kevin Buzzard]

Did you try library_search for eq_compl_of_compl_eq?

[Iocta]

What is the rintros-only version of rintros s ⟨t, ht⟩, cases ht with h,?

[Iocta]

library_search didn't work for eq_compl_of_compl_eq ("excessive memory consumption")

[Kevin Buzzard]

Try looking for the iff version? The rintros version probably replaces ht with (h1 | h2)

[Iocta]

I tried replacing the have/from like simp only [*, not_not, finset.mem_coe, mem_compl_eq, eq_compl_of_compl_eq, h2] at *, but it said invalid simplification lemma 'eq_compl_of_compl_eq'

[Kevin Buzzard]

Indeed that is a useless simp lemma by itself. I'm suggesting you add the full proof ie eq_compl_of_compl_eq h1

[Iocta]

Replacing rintros s ⟨t, ht⟩, cases ht with h, with rintros s ⟨t, ⟨h1 | h2⟩⟩, leaves me with image.png

[Kevin Buzzard]

You can just use simp to close goals, you don't need all this simp only stuff

[Iocta]

I read somewhere that it's bad style to just use simp because the simp rules change over time, so I normally write squeeze_simp and just use whatever it says

[Kevin Buzzard]

You need round brackets like I used, not pointy ones. Sorry I can't help more, I'm not at lean right now.

[Kevin Buzzard]

It's bad style to use simp to not close a goal. If it's solving the goal it's fine.

[Iocta]

can all be done in one line

what are the rules for what's done in a single line?

[Iocta]

btw dunno what's wrong with those ()in the screenshot but it always wraps weird like that when there's a \compl

[Iocta]

Try looking for the iff version?

lemma eq_compl_of_compl_eq (s1 s2: set ℤ) (h : s1ᶜ = s2) (x : ℤ) : x ∈ s1 ↔ x ∈ s2ᶜ :=
begin
library_search,
end

didn't work either

[Eric Wieser]

I think Kevin is describing

lemma eq_compl_iff_compl_eq (s1 s2: set ℤ) :
  s1 = s2ᶜ ↔ s1ᶜ = s2 :=
begin
  library_search,
end

does that work?

[Iocta]

No

[Eric Wieser]

How about the statement function.involutive (has_compl.compl : set X \to set X)?

[Iocta]

If you mean

example (X : Type) : function.involutive (has_compl.compl : set X → set X) := begin
  library_search,
end

then no

[Kevin Buzzard]

It's in there somewhere. Why not just read data.set.basic? Find the section on compl.

[Iocta]

Maybe it's in a form I don't recognize, but I don't see it. https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#lemmas-about-complement

[Kevin Buzzard]

There's also a bunch of stuff in order/boolean_algebra but I can't see it there either. Here are some shorter proofs:

import tactic
import data.set.basic

namespace set

variable {α : Type*}

lemma eq_compl_of_compl_eq {s1 s2: set α} : s1ᶜ = s2 → s1 = s2ᶜ :=
begin
  rintro rfl,
  exact (compl_compl s1).symm,
end

lemma eq_compl_iff_compl_eq (s1 s2 : set α) : s1ᶜ = s2 ↔ s1 = s2ᶜ :=
⟨eq_compl_of_compl_eq, λ h, (eq_compl_of_compl_eq h.symm).symm⟩

end set

[Bryan Gin-ge Chen]

These should definitely be added to mathlib (in order/boolean_algebra).

[Iocta]

Why is the have necessary?

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

open_locale classical
noncomputable theory





structure algebra' (α : Type*) :=
(in_algebra : set α → Prop)
(algebra_empty : in_algebra ∅)
(algebra_compl : ∀ (s : set α), in_algebra s → in_algebra sᶜ)
(algebra_union : ∀ (s1 s2 : set α), in_algebra s1 → in_algebra s2 → in_algebra (s1 ∪ s2))



lemma eq_compl_of_compl_eq (s1 s2: set ℤ) (h : s1ᶜ = s2) : s1 = s2ᶜ :=
begin
ext,
split;
{
  intro h,
  simp only [mem_compl_eq] at *,
  finish,
},
end



example : algebra' ℤ := {
  in_algebra := λs, ∃ (t : finset ℤ), (s = t) ∨ (sᶜ = t),
  algebra_empty :=
  ⟨finset.empty, or.inl rfl⟩,
  algebra_compl := begin
    rintros s ⟨t, ht⟩, cases ht with h,
    { use t, rw [compl_compl], right, exact h, },
    { use t, left, exact ht, }
  end,
  algebra_union := begin
    rintros s1 s2 ⟨t1, (h11 |h12)⟩ ⟨t2, (h21 | h22)⟩,
    {
      use t1 ∪ t2,
      left,
      simp only [finset.coe_union, *],
    },
    {
      use t2.filter (λx, x ∉ s1),
      right,
      rw [compl_union],
      ext,
      simp only [mem_sep_eq, mem_inter_eq, finset.mem_coe, mem_compl_eq, finset.coe_filter],
      split,
      simp only [*, and_imp, finset.mem_coe] at *,
      {
        intros h h',
        split,
        { -- have: s2 = t2ᶜ, from by {  apply eq_compl_of_compl_eq, exact h22, },
          simp [*, eq_compl_of_compl_eq s2, eq_compl_of_compl_eq t2ᶜ] at *,  },
        { exact h, },
      },
      {
        intros h,
        split,
        { exact h.2,  },
        { cases h,
          rw [←mem_compl_eq],
          simp only [*, finset.mem_coe] at *,   },
      },
    },
    {
        use t1.filter (λx, x ∉ s2),
        right,
        rw [compl_union],
        ext,
        split,
        { intro h, simp [*] at *, },
        { intro h, { simp [*, eq_compl_of_compl_eq s1] at *,}, },
    },
    {
        use t1.filter (λx, x ∈ t2),
        right,
        ext,
        simp [*, eq_compl_of_compl_eq s1, eq_compl_of_compl_eq s2] at *,
    },
  end
}


simp_all tactic failed to simplify
state:
s1 s2 : set ℤ,
t1 : finset ℤ,
h11 : s1 = ↑t1,
t2 : finset ℤ,
h22 : s2ᶜ = ↑t2,
x : ℤ,
h : x ∉ t1,
h' : x ∉ s2
⊢ x ∈ t2

[Iocta]

Anyway that's a good reduction in verbosity, but still pretty large

[Damiano Testa]

You may want to double-check, but I think that this is a simplified version of what you had:

lemma compl_eq_iff {α : Type*} (s1 s2 : set α) : s1ᶜ = s2 ↔ s2ᶜ = s1 :=
by refine ⟨_, _⟩; rintros rfl; exact compl_compl _

example : algebra' ℤ := {
  in_algebra := λs, ∃ (t : finset ℤ), (s = t) ∨ (sᶜ = t),
  algebra_empty :=
  ⟨finset.empty, or.inl rfl⟩,
  algebra_compl := begin
    rintro s ⟨t, rfl | h⟩,
    { exact ⟨t, or.inr (compl_compl ↑t)⟩ },
    { exact ⟨t, or.inl h⟩ }
  end,
  algebra_union := begin
    rintro s1 s2 ⟨t1, rfl | h⟩ ⟨t2, rfl | k⟩,
    { exact ⟨t1 ∪ t2, or.inl (finset.coe_union _ _).symm⟩ },
    { rw ← (compl_eq_iff _ _).mp k,
      exact ⟨t2.filter (λx, x ∉ t1), or.inr (ext (λ x, by simp [and_comm]))⟩ },
    { rw ← (compl_eq_iff _ _).mp h,
      exact ⟨t1.filter (λ x, x ∉ t2), or.inr (ext (λ x, by simp [and_comm]))⟩ },
    { rw ← (compl_eq_iff _ _).mp h,
      exact ⟨t1.filter (λx, x ∉ s2), or.inr (ext (λ x, by simp [and_comm]))⟩ },
  end }

[Damiano Testa]

Also, while I have not worked with it, it might be better to make implicit some of the inputs in your definition of algebra':

structure algebra' (α : Type*) :=
(in_algebra : set α → Prop)
(algebra_empty : in_algebra ∅)
(algebra_compl : ∀ {s : set α}, in_algebra s → in_algebra sᶜ)  -- made `s` implicit
(algebra_union : ∀ {s1 s2 : set α}, in_algebra s1 → in_algebra s2 → in_algebra (s1 ∪ s2))  -- made `s1 s2` implicit

[Iocta]

That's quite an improvement! Thanks @Damiano Testa

[Iocta]

How can I express "the set of finite disjoint unions of sets in S"?
image.png

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

open_locale classical
noncomputable theory

structure algebra' (α : Type*) :=
(in_algebra : set α → Prop)
(algebra_empty : in_algebra ∅)
(algebra_compl : ∀ (s : set α), in_algebra s → in_algebra sᶜ)
(algebra_union : ∀ (s1 s2 : set α), in_algebra s1 → in_algebra s2 → in_algebra (s1 ∪ s2))

structure semialgebra (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), sUnion (c : set (set α)) = sᶜ)

[Kevin Buzzard]

You could define it recursively. Or you might want to check that the finite disjoint unions are just the same as the finite unions, which would be easier to define and work with -- I think they are.

[Iocta]

by 'check that ...' do you mean check that this result holds for finite unions in general?

[Iocta]

(deleted)

[Kevin Buzzard]

I can't make sense of your lemma 1.1.3. How does one see that "the definition of S implies S_i^c \in S-bar"? I can't immediately see how to deduce it from your formal definition of semialgebra -- you know that the complement is a union of things in the semialgebra but you don't know the union is disjoint, right?

[Kevin Buzzard]

For me, the algebra generated by the semialgebra seems to naturally be the finite union of elements of the semialgebra and then the proof that it's an algebra goes through; moreover it's clearly the smallest algebra containing the semialgebra, at least if we go via the definitions you have formalised.

[Iocta]

This text does use 'disjoint' in the definition of semialgebra image.png
so maybe I should try to include that in my lean semialgebra definition

[Iocta]

Or maybe that's unnecessary complication

[Iocta]

Is that like this?

structure semialgebra' (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), (∀ (x  ∈ c) (y ∈ c),  x ∩ y = ∅) ∧ sUnion (c : set (set α)) = sᶜ)

[Kevin Buzzard]

If you change the definition from the book then you'll have a different definition. Your definition of pairwise disjoint above is incorrect because you can have x=y. There might already be a way of saying "pairwise disjoint" in mathlib but I don't personally know it

[Eric Wieser]

docs#complete_lattice.independent I think is equivalent for sets?