## Stream: new members

### Topic: semialgebra setminus

#### Iocta (Mar 16 2021 at 20:27):

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 (Mar 16 2021 at 20:45):

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 (Mar 16 2021 at 20:45):

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 (Mar 16 2021 at 20:52):

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

#### Iocta (Mar 16 2021 at 21:05):

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 (Mar 16 2021 at 22:06):

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

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

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 (Mar 16 2021 at 22:13):

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

#### Iocta (Mar 17 2021 at 22:46):

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 (Mar 17 2021 at 22:59):

Are you sure you want heq I as your in_semi_algebra?

#### Eric Wieser (Mar 17 2021 at 22:59):

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

#### Eric Wieser (Mar 17 2021 at 23:01):

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 (Mar 17 2021 at 23:03):

That looks more right, I'll try that

#### Iocta (Mar 17 2021 at 23:05):

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 (Mar 17 2021 at 23:51):

Oh yeah, I forgot what closed meant!

#### Iocta (Mar 18 2021 at 19:36):

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 (Mar 18 2021 at 19:37):

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 (Mar 18 2021 at 19:37):

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

It's in h2

#### Kevin Buzzard (Mar 18 2021 at 19:49):

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 (Mar 18 2021 at 19:52):

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 (Mar 18 2021 at 19:53):

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

#### Kevin Buzzard (Mar 18 2021 at 19:54):

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

#### Kevin Buzzard (Mar 18 2021 at 19:54):

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 (Mar 18 2021 at 19:58):

That goal looks untrue to me

#### Kevin Buzzard (Mar 18 2021 at 20:00):

∃ (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 (Mar 18 2021 at 20:03):

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

#### Kevin Buzzard (Mar 18 2021 at 20:05):

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 (Mar 18 2021 at 20:08):

Oh that's much nicer

#### Kevin Buzzard (Mar 18 2021 at 20:09):

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

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

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 (Mar 18 2021 at 20:13):

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.

Iic?

#### Kevin Buzzard (Mar 18 2021 at 20:14):

yes it could well be that

docs#set.Iic

#### Kevin Buzzard (Mar 18 2021 at 20:15):

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

#### Iocta (Mar 18 2021 at 20:17):

I'm trying to copy image.png

#### Iocta (Mar 18 2021 at 20:18):

But one dimensional for now

#### Kevin Buzzard (Mar 18 2021 at 20:19):

note the possibility that a and b can be infinity.

#### Iocta (Mar 18 2021 at 20:19):

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 (Mar 18 2021 at 20:19):

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

(deleted)

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

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 (Mar 18 2021 at 20:32):

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 (Mar 18 2021 at 20:44):

Isn't that what I posted earlier?

#### Iocta (Mar 18 2021 at 20:49):

It's very close, also changed real to ereal

#### Iocta (Mar 19 2021 at 00:31):

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 (Mar 19 2021 at 00:42):

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

Yeah that was it

#### Iocta (Mar 19 2021 at 08:44):

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 (Mar 19 2021 at 08:51):

I think it's true

#### Johan Commelin (Mar 19 2021 at 08:55):

Does ext get you started?

#### Eric Wieser (Mar 19 2021 at 11:01):

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 (Mar 19 2021 at 11:04):

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 (Mar 19 2021 at 11:04): Along with the other three variants of o and c #### Iocta (Mar 19 2021 at 21:52): 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 (Mar 19 2021 at 21:59):

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

#### Eric Wieser (Mar 19 2021 at 22:00):

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

#### Eric Wieser (Mar 20 2021 at 10:14):

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 (Mar 20 2021 at 20:43):

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 (Mar 20 2021 at 20:50):

rfl is like introducing h then immediately doing rw h

#### Eric Wieser (Mar 20 2021 at 20:50):

Although that's a bit of a simplification

#### Iocta (Mar 20 2021 at 20:51):

Whereas the _ is just introducing h?

#### Iocta (Mar 20 2021 at 21:00):

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


does work

#### Eric Wieser (Mar 20 2021 at 21:37):

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

#### Iocta (Mar 21 2021 at 04:46):

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 (Mar 21 2021 at 08:04):

"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 (Mar 21 2021 at 08:04):

intros, cases can be done with rintro

#### Kevin Buzzard (Mar 21 2021 at 08:05):

Did you try library_search for eq_compl_of_compl_eq?

#### Iocta (Mar 21 2021 at 08:16):

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

#### Iocta (Mar 21 2021 at 08:17):

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

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

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

#### Iocta (Mar 21 2021 at 08:25):

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 (Mar 21 2021 at 08:27):

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 (Mar 21 2021 at 08:28):

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

#### Kevin Buzzard (Mar 21 2021 at 08:28):

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

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

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 (Mar 21 2021 at 08:29):

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 (Mar 21 2021 at 08:30):

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

#### Iocta (Mar 21 2021 at 08:33):

can all be done in one line

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

#### Iocta (Mar 21 2021 at 08:34):

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

#### Iocta (Mar 21 2021 at 08:36):

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 (Mar 21 2021 at 09:13):

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?

No

#### Eric Wieser (Mar 21 2021 at 18:52):

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

#### Iocta (Mar 21 2021 at 18:58):

If you mean

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


then no

#### Kevin Buzzard (Mar 21 2021 at 19:08):

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

#### Iocta (Mar 21 2021 at 20:04):

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 (Mar 21 2021 at 20:41):

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 (Mar 21 2021 at 20:48):

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

#### Iocta (Mar 21 2021 at 21:11):

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 (Mar 21 2021 at 21:13):

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

#### Damiano Testa (Mar 22 2021 at 14:16):

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 (Mar 22 2021 at 14:35):

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 (Mar 22 2021 at 19:58):

That's quite an improvement! Thanks @Damiano Testa

#### Iocta (Mar 24 2021 at 19:14):

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 (Mar 24 2021 at 19:19):

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 (Mar 24 2021 at 19:26):

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

(deleted)

#### Kevin Buzzard (Mar 24 2021 at 19:50):

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 (Mar 24 2021 at 19:51):

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 (Mar 24 2021 at 20:51):

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 (Mar 24 2021 at 20:51):

Or maybe that's unnecessary complication

#### Iocta (Mar 24 2021 at 21:06):

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 (Mar 25 2021 at 08:12):

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 (Mar 25 2021 at 08:33):

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

Last updated: May 13 2021 at 00:41 UTC