Do nested sets containing all elements include set.univ?

Stream: new members

[Eric Wieser]

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?

[Reid Barton]

it's not true

[Eric Wieser]

Provably false?

[Anne Baanen]

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

[Eric Wieser]

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]

What you are saying is nonsense

[Kevin Buzzard]

Infinity is not a number

[Kevin Buzzard]

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

[Anne Baanen]

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

[Kevin Buzzard]

Sure.

[Kevin Buzzard]

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

[Eric Wieser]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

Yes :-)

[Kevin Buzzard]

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]

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]

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.