Zulip Chat Archive

Stream: new members

Topic: smallest subset


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 09:27):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 09:28):

this doesn't need any measurable space stuff

view this post on Zulip Mario Carneiro (Oct 21 2020 at 09:29):

there is a version of this proof in set_theory.zfc

view this post on Zulip Iocta (Oct 21 2020 at 09:29):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 09:29):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Iocta (Oct 21 2020 at 09:31):

oh crap :-)

view this post on Zulip Mario Carneiro (Oct 21 2020 at 09:33):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 09:33):

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

view this post on Zulip Iocta (Oct 21 2020 at 09:35):

you mean intersect s = {a}?

view this post on Zulip Mario Carneiro (Oct 21 2020 at 09:35):

yes

view this post on Zulip Mario Carneiro (Oct 21 2020 at 09:36):

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

view this post on Zulip Kenny Lau (Oct 21 2020 at 09:38):

that holds if a has type set X

view this post on Zulip Kenny Lau (Oct 21 2020 at 09:38):

so s has type set $ set $ set X

view this post on Zulip Kenny Lau (Oct 21 2020 at 09:39):

to emulate ZFC, add in continuously more prefixes of set

view this post on Zulip Mario Carneiro (Oct 21 2020 at 09:39):

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

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Oct 21 2020 at 09:40):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 22 2020 at 06:42):

src#Set.pair_inj

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 22 2020 at 07:01):

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

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

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

view this post on Zulip Kevin Buzzard (Oct 22 2020 at 07:02):

Oh wow so it is pretty long!

view this post on Zulip Mario Carneiro (Oct 22 2020 at 07:02):

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

view this post on Zulip Kevin Buzzard (Oct 22 2020 at 07:02):

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

view this post on Zulip 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

view this post on Zulip 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}}\{\{0, a\}, \{1, b\}\} is simpler to prove the pairing theorem), but kuratowski is a shorter definition

view this post on Zulip Kevin Buzzard (Oct 22 2020 at 07:06):

Maybe he should have said automation over honest toil

view this post on Zulip Mario Carneiro (Oct 22 2020 at 07:07):

This proof is certainly sledgehammerable

view this post on Zulip Mario Carneiro (Oct 22 2020 at 07:08):

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

view this post on Zulip Mario Carneiro (Oct 22 2020 at 07:09):

it's also NSFTT

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 24 2020 at 08:07):

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

view this post on Zulip Johan Commelin (Oct 24 2020 at 08:07):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 24 2020 at 08:14):

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

view this post on Zulip Johan Commelin (Oct 24 2020 at 08:14):

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

view this post on Zulip Iocta (Oct 24 2020 at 08:15):

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

view this post on Zulip Johan Commelin (Oct 24 2020 at 08:15):

The u

view this post on Zulip 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.

view this post on Zulip Iocta (Oct 24 2020 at 08:18):

ah ok I see

view this post on Zulip 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

view this post on Zulip Iocta (Oct 24 2020 at 08:29):

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

view this post on Zulip Johan Commelin (Oct 24 2020 at 08:33):

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

view this post on Zulip Johan Commelin (Oct 24 2020 at 08:34):

The : type part is left out

view this post on Zulip Iocta (Oct 24 2020 at 08:34):

ohhh

view this post on Zulip Iocta (Oct 24 2020 at 08:35):

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


Last updated: May 14 2021 at 12:18 UTC