Zulip Chat Archive
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
Iocta (Oct 21 2020 at 09:31):
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}?
Mario Carneiro (Oct 21 2020 at 09:35):
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 nonsets
Mario Carneiro (Oct 21 2020 at 09:40):
it also doesn't really work if you have illstratified 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.
Mario Carneiro (Oct 22 2020 at 06:42):
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'$.
 $x = x'$: Since $\{x\}\in p$, $\{x\}=\{x'\}$ (so $x = x'$), or $\{x\}=\{x',y'\}$, in which case $x'\in\{x\}$ so $x = x'$.
 $y=x\to y=y'$. Substitute $y$ with $x$, then $p=\{\{x\}\}$ so $\{x', y'\}\in\{\{x\}\}$ so $y'\in\{x\}$.

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
Mario Carneiro (Oct 22 2020 at 07:09):
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/leanprovercommunity/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
.
Iocta (Oct 24 2020 at 08:18):
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://leanprovercommunity.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
Iocta (Oct 24 2020 at 08:34):
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