Zulip Chat Archive

Stream: new members

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


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

view this post on Zulip Reid Barton (Nov 10 2020 at 13:14):

it's not true

view this post on Zulip Eric Wieser (Nov 10 2020 at 13:15):

Provably false?

view this post on Zulip Anne Baanen (Nov 10 2020 at 13:16):

The list {}, {0}, {0, 1}, {0, 1, 2}, ... is a counterexample for , no?

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

view this post on Zulip Kevin Buzzard (Nov 10 2020 at 13:32):

What you are saying is nonsense

view this post on Zulip Kevin Buzzard (Nov 10 2020 at 13:32):

Infinity is not a number

view this post on Zulip Kevin Buzzard (Nov 10 2020 at 13:33):

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

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

view this post on Zulip Kevin Buzzard (Nov 10 2020 at 13:34):

Sure.

view this post on Zulip Kevin Buzzard (Nov 10 2020 at 13:35):

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

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

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

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

view this post on Zulip 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 an=1/na_n=1/n and spend forever carefully talking about limits, and then still you'll get students writing limnan=a=1/=0\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.

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

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

view this post on Zulip Eric Wieser (Nov 10 2020 at 14:47):

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

view this post on Zulip Kevin Buzzard (Nov 10 2020 at 14:47):

Yes :-)

view this post on Zulip Kevin Buzzard (Nov 10 2020 at 14:49):

Somehow the standard problem with "letting n=infinity" is that if you have a sequence like an=(1)na_n=(-1)^n then aa_\infty now really doesn't make any sense. In the 1/n1/n situation there is a reasonable interpretation of n=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 AnA_n are increasing, AnAn+1A_n\subseteq A_{n+1}, it is reasonable to interpret AA_{\infty} as nNAn\bigcup_{n\in\mathbb{N}}A_n, but this trick does not work in general; e.g. if An={n}NA_n=\{n\}\subseteq\mathbb{N} then AA_{\infty} has no reasonable interpretation as a subset of N\mathbb{N}.

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

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