## 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)is?

it's not true

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:

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

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