smallest subset

Stream: new members

[Iocta]

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]

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

[Mario Carneiro]

this doesn't need any measurable space stuff

[Mario Carneiro]

there is a version of this proof in set_theory.zfc

[Iocta]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Iocta]

oh crap :-)

[Mario Carneiro]

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

[Mario Carneiro]

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

[Iocta]

you mean intersect s = {a}?

[Mario Carneiro]

yes

[Mario Carneiro]

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

[Kenny Lau]

that holds if a has type set X

[Kenny Lau]

so s has type set $ set $ set X

[Kenny Lau]

to emulate ZFC, add in continuously more prefixes of set

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Iocta]

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]

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]

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]

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]

src#Set.pair_inj

[Mario Carneiro]

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]

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]

Oh wow so it is pretty long!

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

“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]

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]

Maybe he should have said automation over honest toil

[Mario Carneiro]

This proof is certainly sledgehammerable

[Mario Carneiro]

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]

it's also NSFTT

[Iocta]

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]

{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]

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

[Johan Commelin]

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

[Iocta]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Iocta]

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

[Johan Commelin]

The u

[Johan Commelin]

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]

ah ok I see

[Iocta]

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]

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

[Johan Commelin]

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

[Johan Commelin]

The : type part is left out

[Iocta]

ohhh

[Iocta]

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