# Zulip Chat Archive

## Stream: new members

### Topic: Do nested sets containing all elements include set.univ?

#### Eric Wieser (Nov 10 2020 at 13:10):

I have an indexed collection of sets `sets`

over `A`

, such that each set is a superset of the one before it. I also know that for every element of `A`

, there is at least one set in `sets`

that contains it.

Is it true that one of my sets must be `set.univ`

?

```
example (A : Type*) (sets : ℕ → set A) (h_mono : monotone sets) (h : ∀ a, ∃ n, a ∈ sets n):
∃ n, ∀ a, a ∈ sets n := sorry
```

On the one hand, this feels like it requires me to conjure an `infinity : ℕ`

. On the other hand, if I have the proof that every element of `a`

has a corresponding `i`

, can I just pick the maximum of those (infinitely many)`i`

s?

#### Reid Barton (Nov 10 2020 at 13:14):

it's not true

#### Eric Wieser (Nov 10 2020 at 13:15):

Provably false?

#### Anne Baanen (Nov 10 2020 at 13:16):

The list `{}, {0}, {0, 1}, {0, 1, 2}, ...`

is a counterexample for `ℕ`

, no?

#### Eric Wieser (Nov 10 2020 at 13:31):

I think my issue is that I'm inclined to hand-wave and say that "the last element of that list contains all the integers", and I don't know whether that hand-waving is allowed by the axioms

#### Kevin Buzzard (Nov 10 2020 at 13:32):

What you are saying is nonsense

#### Kevin Buzzard (Nov 10 2020 at 13:32):

Infinity is not a number

#### Kevin Buzzard (Nov 10 2020 at 13:33):

There is no last element of that list because there is no biggest number

#### Anne Baanen (Nov 10 2020 at 13:34):

If the list were indexed by a successor ordinal though, then there would be a biggest number :upside_down:

#### Kevin Buzzard (Nov 10 2020 at 13:34):

Sure.

#### Kevin Buzzard (Nov 10 2020 at 13:35):

But it's indexed by the naturals, which is not a successor ordinal

#### Eric Wieser (Nov 10 2020 at 14:21):

It confuses me a little that I can prove `(⋃ (i : ℕ), sets i) = set.univ := set.eq_univ_of_forall (λ x, set.mem_Union.mpr (h x))`

, yet despite knowing that only one element of that union is relevant, I can't show that it exists

#### Kevin Buzzard (Nov 10 2020 at 14:36):

You seem to have a fundamental misunderstanding of the infinite. A cofinal system of elements of the union are relevant. Your claim that "only one element of that union is relevant" is simply **mathematically wrong**. Every element of Anne's example is finite.

#### Adam Topaz (Nov 10 2020 at 14:40):

Another way to put all this is that given any element of `set.univ`

, there exists some member in the family of subsets which contains that element, but that member *will depend* on the original element. So it's not true (as in Anne's example) that there exists a single set in the family which works for *all* elements of `set.univ`

.

#### Kevin Buzzard (Nov 10 2020 at 14:45):

Note that I see this all the time with undergraduates in analysis -- this is a common misconception for people without a university maths background. We define sequences $a_n=1/n$ and spend forever carefully talking about limits, and then still you'll get students writing $\lim_{n\to\infty}a_n=a_{\infty}=1/\infty=0$. This handwavy approach might be OK in some situations but unfortunately it cannot be turned into a rigorous approach which has all the properties you expect it to have, and so has to be avoided.

#### Eric Wieser (Nov 10 2020 at 14:46):

I'd probably make the slightly weaker description that I don't claim to have an understanding of the infinite at all, and this was me looking to borrow the understanding of someone who does :)

#### Kevin Buzzard (Nov 10 2020 at 14:46):

I am teaching analysis right now, so already have my hackles up about all this :-) The number of times I am going to have to say "infinity is not a number" this term...

#### Eric Wieser (Nov 10 2020 at 14:47):

As a follow-up question - presumably my original statement is true with `[fintype A]`

?

#### Kevin Buzzard (Nov 10 2020 at 14:47):

Yes :-)

#### Kevin Buzzard (Nov 10 2020 at 14:49):

Somehow the standard problem with "letting n=infinity" is that if you have a sequence like $a_n=(-1)^n$ then $a_\infty$ now really doesn't make any sense. In the $1/n$ situation there is a reasonable interpretation of $n=\infty$ which makes it all work, but the problem is that it doesn't work in general. The sets situation you're in is similar --because your sets $A_n$ are increasing, $A_n\subseteq A_{n+1}$, it is reasonable to interpret $A_{\infty}$ as $\bigcup_{n\in\mathbb{N}}A_n$, but this trick does not work in general; e.g. if $A_n=\{n\}\subseteq\mathbb{N}$ then $A_{\infty}$ has no reasonable interpretation as a subset of $\mathbb{N}$.

#### Kevin Lacker (Nov 10 2020 at 18:36):

kind of an off topic comment but I really liked this book - https://www.amazon.com/Everything-More-Compact-History-Infinity/dp/0393339289 - about the history of mathematicians trying to figure out whether infinity was a legitimate number or not and how to deal with it or even think about it. once I saw how these smart people in the past were confused by it, i had more sympathy for modern people that find it unintuitive

#### Kevin Buzzard (Nov 10 2020 at 19:38):

I see smart first year undergraduates confused by it year after year. We have some system now which deals with it adequately enough and it's just a case of drummimg the modern approach into their heads.

Last updated: May 16 2021 at 05:21 UTC