## Stream: new members

### Topic: smallest subset

#### Iocta (Oct 21 2020 at 09:26):

I have {{a},{a,b}} and I want to refer to the {a} part, identifying it as the smallest element. How can I extract it? The plan is to show "the only element of the smallest subset must be preserved on both sides of the equality, so a=c".

example
(a b c d : Ω)
(s t : set(set Ω))
(hs: s = {{a}, {a,b}})
(ht: t = {{c}, {c,d}}) :
s = t ↔ a = c ∧ b = d :=
begin
split,
{
intro h,
rw [hs, ht] at h,
split,
{
-- Ω: Type u_1
-- _inst_1: measurable_space Ω
-- abcd: Ω
-- st: set (set Ω)
-- hs: s = {{a}, {a, b}}
-- ht: t = {{c}, {c, d}}
-- h: {{a}, {a, b}} = {{c}, {c, d}}
-- ⊢ a = c
sorry,
-- s = t.
-- The smallest element min(s,key=size) of s equals the smallest element of t.
-- The only element of that minimum equals its counterpart from t.
-- a = c.
},
{
-- After replacing a = c in t, apply a similar argument but with the largest subset.
sorry,
},
}
end


#### Mario Carneiro (Oct 21 2020 at 09:27):

what does smallest have to do with anything? This is just injectivity of kuratowski pairs

#### Mario Carneiro (Oct 21 2020 at 09:28):

this doesn't need any measurable space stuff

#### Mario Carneiro (Oct 21 2020 at 09:29):

there is a version of this proof in set_theory.zfc

#### Iocta (Oct 21 2020 at 09:29):

I was gonna say "{a} is the only one that's that size, namely one element"

#### Mario Carneiro (Oct 21 2020 at 09:29):

I don't think we have it for set (set A) though

#### Mario Carneiro (Oct 21 2020 at 09:30):

it's just a basic logic proof, you go through the cases of how two pairs can be equal

#### Mario Carneiro (Oct 21 2020 at 09:30):

besides it's not true that it's the only one of that size, {a,b} can have size 1 if a = b

oh crap :-)

#### Mario Carneiro (Oct 21 2020 at 09:33):

One way to define it is to note that Union s = {a}

#### Mario Carneiro (Oct 21 2020 at 09:33):

so s = t -> {a} = {c} and hence a = c by injectivity of singletons

#### Iocta (Oct 21 2020 at 09:35):

you mean intersect s = {a}?

yes

#### Mario Carneiro (Oct 21 2020 at 09:36):

in zfc you can just write a = ⋃ ⋂ s but that doesn't hold in type theory

#### Kenny Lau (Oct 21 2020 at 09:38):

that holds if a has type set X

#### Kenny Lau (Oct 21 2020 at 09:38):

so s has type set $set$ set X

#### Kenny Lau (Oct 21 2020 at 09:39):

to emulate ZFC, add in continuously more prefixes of set

#### Mario Carneiro (Oct 21 2020 at 09:39):

that embeds ZFC, but it doesn't let you prove things about non-sets

#### Mario Carneiro (Oct 21 2020 at 09:40):

it also doesn't really work if you have ill-stratified formulas like the definition of "transitive set"

#### Mario Carneiro (Oct 21 2020 at 09:40):

(which says ∀ x ∈ S, x ⊆ S)

#### Kevin Buzzard (Oct 21 2020 at 09:48):

Aren't transitive sets just some combinatorial trick to enable you to define ordinals? I don't think I've seen them anywhere else.

#### Mario Carneiro (Oct 21 2020 at 10:03):

sure, most things that use sets in this way are solidly in the domain of "set theory" as distinct from other disciplines

#### Mario Carneiro (Oct 21 2020 at 10:04):

In addition to being used to define ordinals and cardinals, transitive sets are often used for building models of set theory

#### Mario Carneiro (Oct 21 2020 at 10:05):

anything about well founded recursion generally boils down to this because in ZFC epsilon is the well founded relation

#### Iocta (Oct 21 2020 at 22:26):

How can I fill the first sorry?

import data.real.basic
import tactic.fin_cases
import data.set.basic
import data.finset.basic
import data.finset.intervals
import algebra.big_operators

open set real

open_locale big_operators

noncomputable theory

universe u

example
(a b c d : ℝ)
(s t : set(set ℝ))
(hs: s = {{a}, {a,b}})
(ht: t = {{c}, {c,d}}) :
s = t ↔ a = c ∧ b = d :=
begin
split,
{
intro h,
split,
{

have s_inter_eq_singleton_a: (⋂ z ∈ s, z) = {a},
{
-- For every subset z of s, a is in it.
-- If x is in every subset of s, x = a.
ext1,
split,
{
intro h1,
-- abcd: ℝ
-- st: set (set ℝ)
-- hs: s = {{a}, {a, b}}
-- ht: t = {{c}, {c, d}}
-- h: s = t
-- x: ℝ
-- h1: x ∈ ⋂ (z : set ℝ) (H : z ∈ s), z
-- ⊢ x ∈ {a}
sorry,
},
{
intro h1,
sorry,
}
},
have t_inter_eq_singleton_c: (⋂ z ∈ t, z) = {c},
{
-- For every subset z of t, c is in it.
-- If x is in every subset of t, x = c.
sorry,
},
have inter_eq: (⋂ z ∈ s, z) = (⋂ z ∈ t, z),
{
ext1,
split; {
intro h1,
simp only [mem_Inter] at *,
intros i hi,
specialize h1 i,
finish,
},
},
finish,
},
{
sorry,
},
}
end


#### Kevin Buzzard (Oct 21 2020 at 22:44):

Is there set.mem_Inter or set.mem_sInter? That would be the sort of name I'd guess for what you need to rewrite with at h1.

#### Iocta (Oct 21 2020 at 23:56):

I'm not even done but this is really labor intensive for such a minor statement, and the automation tactics aren't helping me out that much. Am I going about this the wrong way, or just need more practice to get faster?

example
(a b c d : ℝ)
(s t : set(set ℝ))
(hs: s = {{a}, {a,b}})
(ht: t = {{c}, {c,d}}) :
s = t ↔ a = c ∧ b = d :=
begin
split,
{
intro h,

have a_eq_c: a = c, {

have s_inter_eq_singleton_a: (⋂ z ∈ s, z) = {a},
{
-- For every subset z of s, a is in it.
-- If x is in every subset of s, x = a.
ext1,
split,
{
intro h1,
rw [mem_Inter] at h1,
specialize h1 {a},
simp only [mem_singleton_iff, mem_Inter] at h1,
rw [hs] at h1,
simp only [forall_prop_of_true, true_or, eq_self_iff_true, mem_insert_iff] at h1,
simp only [mem_singleton_iff],
exact h1,
},
intro h2,
simp,
intros subset hsubset,
simp only [mem_singleton_iff] at h2,
rw [hs] at hsubset,
cases hsubset,
{
rw [hsubset],
exact mem_singleton_iff.mpr h2,
},
{
simp only [mem_singleton_iff] at hsubset,
rw [hsubset],
rw h2,
exact mem_insert a {b},
}
},
have t_inter_eq_singleton_c: (⋂ z ∈ t, z) = {c},
{
-- For every subset z of t, c is in z.
-- If x is in every subset of t, x = c.
sorry,
},
have inter_eq: (⋂ z ∈ s, z) = (⋂ z ∈ t, z),
{
ext1,
split; {
intro h1,
simp only [mem_Inter] at *,
intros i hi,
specialize h1 i,
finish,
},
},
finish,

},
split,
{        exact a_eq_c    },
{
rw [a_eq_c] at *,
rw [hs, ht] at h,
have: {{c,b}} = {{c,d}},
{    sorry,        },
have: {c,b} = {c,d}, sorry,
sorry,
},
}
end


#### Kevin Buzzard (Oct 22 2020 at 06:20):

Mario pointed out that this was already proved in the ZFC part of mathlib. Did you look at what he did there? This proof should be no more than a few lines I suspect.

src#Set.pair_inj

#### Mario Carneiro (Oct 22 2020 at 06:46):

One obvious first move in the proof is to get rid of s and t. I find it is good practice to always use subst as early as possible, because there are simp lemmas about a \in {b, c} but not a \in s

#### Mario Carneiro (Oct 22 2020 at 07:01):

Here's the informalized proof: Suppose $p:=\{\{x\}, \{x, y\}\} = \{\{x'\}, \{x', y'\}\}$; we claim $x=x'\wedge y=y'$.

1. $x = x'$: Since $\{x\}\in p$, $\{x\}=\{x'\}$ (so $x = x'$), or $\{x\}=\{x',y'\}$, in which case $x'\in\{x\}$ so $x = x'$.
2. $y=x\to y=y'$. Substitute $y$ with $x$, then $p=\{\{x\}\}$ so $\{x', y'\}\in\{\{x\}\}$ so $y'\in\{x\}$.
3. Substitute $x'$ with $x$ by (1). It remains to show $y=y'$. Now $\{x,y\}\in p$, so $\{x,y\}=\{x\}$ or $\{x,y\}=\{x,y'\}$.

• If $\{x,y\}=\{x\}$ then $y\in \{x\}$ so we are done by (2).
• If $\{x,y\}=\{x,y'\}$ then $y\in\{x,y'\}$, and if $y=x$ then we are done by (2), else $y=y'$ and we are done.

#### Kevin Buzzard (Oct 22 2020 at 07:02):

Oh wow so it is pretty long!

#### Mario Carneiro (Oct 22 2020 at 07:02):

it is one of the more complicated pure logic proofs I know

#### Kevin Buzzard (Oct 22 2020 at 07:02):

You can see why it's best to do maths in type theory :-)

#### Mario Carneiro (Oct 22 2020 at 07:03):

“The method of 'postulating' what we want has many advantages ; they are the same as the advantages of theft over honest toil.” --Bertrand Russell

#### Mario Carneiro (Oct 22 2020 at 07:06):

I think there are simpler proofs if you want any pairing operator for which it's true (for example $\{\{0, a\}, \{1, b\}\}$ is simpler to prove the pairing theorem), but kuratowski is a shorter definition

#### Kevin Buzzard (Oct 22 2020 at 07:06):

Maybe he should have said automation over honest toil

#### Mario Carneiro (Oct 22 2020 at 07:07):

This proof is certainly sledgehammerable

#### Mario Carneiro (Oct 22 2020 at 07:08):

there is an even shorter definition $\{a, \{a, b\}\}$, but the proof that this thing satisfies the pairing theorem requires the axiom of foundation, it's not pure logic

it's also NSFTT

#### Iocta (Oct 24 2020 at 08:02):

What are {p} and Set.{u} syntax in @[simp] theorem mem_pair_sep {p} {x y z : Set.{u}}? https://github.com/leanprover-community/mathlib/blob/2987a49/src/set_theory/zfc.lean#L519

#### Johan Commelin (Oct 24 2020 at 08:06):

{p} is an ordinary variable, of which the type isn't specified. So Lean has to figure it out from whatever follows afterwards

#### Johan Commelin (Oct 24 2020 at 08:07):

the u in Set.{u} is a universe variable

#### Johan Commelin (Oct 24 2020 at 08:07):

It means that you want to explicitly set the (first) universe parameter of Set to u.

#### Iocta (Oct 24 2020 at 08:12):

Looks like Set is defined

def Set : Type (u+1) := quotient pSet.setoid.{u}


how does the Set.{u} syntax relate to that signature? I guess it's somehow replacing the u in Type (u+1)

#### Johan Commelin (Oct 24 2020 at 08:13):

Right, so you could use Set.{0} if you want to pin down that u to 0.

#### Johan Commelin (Oct 24 2020 at 08:14):

Or you could write Set.{v} to pin it down to v

#### Johan Commelin (Oct 24 2020 at 08:14):

Assuming you have universe v somewhere near the top of your file

#### Iocta (Oct 24 2020 at 08:15):

what about that Type (u+1) makes it settable via the .{u} syntax?

#### Johan Commelin (Oct 24 2020 at 08:15):

The u

#### Johan Commelin (Oct 24 2020 at 08:17):

Type takes a universe argument. Universe arguments are special, they aren't regular arguments, they don't have a type. Type is not a function universe_arguments -> something.

ah ok I see

#### Iocta (Oct 24 2020 at 08:27):

Why when I put cursor after the comma in have ae := ext_iff.2 H, do I see ae: ∀ (z : Set), z ∈ x.pair y ↔ z ∈ x'.pair y' in context? Shouldn't it only appear after the next comma? https://leanprover-community.github.io/mathlib_docs/find/Set.pair_inj/src

#### Iocta (Oct 24 2020 at 08:29):

usually I see have prop: type, reason,. but here it's something else?

#### Johan Commelin (Oct 24 2020 at 08:33):

@Iocta Note that this is have ae :=, so whatever follows := is already reason

#### Johan Commelin (Oct 24 2020 at 08:34):

The : type part is left out

ohhh

#### Iocta (Oct 24 2020 at 08:35):

it's another one of those let/set/...

Last updated: May 14 2021 at 12:18 UTC