[Merged by Bors] - feat(data/real/cardinality): cardinalities of intervals of reals

[jsm28]

Use the existing result mk_real to deduce corresponding results for
all eight kinds of intervals of reals.

It's convenient for this result to add a new lemma to
data.set.intervals.image_preimage about the image of an interval
under inv. Just as there are only a few results there about images
of intervals under multiplication rather than a full set, so I just
added the result I needed rather than all the possible variants. (I
think there are something like 36 reasonable variants of that lemma
that could be stated, for (image or preimage - the same thing in this
case, but still separate statements) x (interval in positive or
negative reals) x (end closer to 0 is 0 (open), nonzero (open) or
nonzero (closed)) x (other end is open, closed or infinite).)

---

[urkud]

It would be nice to have equivs between open intervals (finite or infinite) and the whole line, and equality of cardinalities in other cases. Though feel free to postpone it to another PR.

[fpvandoorn]

• I think it's indeed good to not add all variants of image_inv_Ioo_0_left. (After [Merged by Bors] - feat(algebra/pointwise): make instances global #3240 simp will at least simplify some of the variants)
• I would prefer if you proved that the cardinality of all these intervals is the continuum (2 ^ omega.{0}), instead of "not countable". That is hopefully not much harder.

[jsm28]

The countable API is convenient for these proofs, using countable.union, countable.image, countable_singleton, countable.mono. To adapt these proofs to show the exact cardinality, we'd need those properties of countable instead for the predicate that a set has cardinality < 2 ^ omega.{0}. Of course they're true for any predicate that the cardinality of a set is less than, or less than or equal to, some given infinite cardinal, but have we got any equivalent of countable.union for that case?

[jcommelin]

Can't you use Cantor–Bernstein? You need to build an injection from real to Ioo a b, and then you're basically done.

[jsm28]

There are plenty of possible ways of proving it, including building up some arbitrary injection piecewise using inv, or proving injectivity of real.tanh as a standard function sometimes used for that purpose, but I was hoping for some argument that's short and not too ugly.

[fpvandoorn]

The countable API is convenient for these proofs, using countable.union, countable.image, countable_singleton, countable.mono. To adapt these proofs to show the exact cardinality, we'd need those properties of countable instead for the predicate that a set has cardinality < 2 ^ omega.{0}. Of course they're true for any predicate that the cardinality of a set is less than, or less than or equal to, some given infinite cardinal, but have we got any equivalent of countable.union for that case?

The API for cardinalities is also pretty good. There is (in the cardinal namespace, in set_theory.cardinal): mk_image_le, mk_image_eq (for injective maps), mk_singleton, mk_le_mk_of_subset.
mk_union_le is missing, but should be a one-liner away from mk_union_add_mk_inter (please add it!). This can be used in combination with add_eq_max (in set_theory.ordinal) or one of its corollaries.
There will be some extra work, like proving that 1 < 2 ^ omega.{0} (lt_trans one_lt_omega (cantor _)) and showing actual equalities (using le_antisymm + mk_set_le). But you should be able to use the same proof structure.

[jsm28]

Thanks for the hints. I've converted the changes to prove cardinalities rather than "not countable", with the same proof structure. (not_countable_real_Ioo was the actual lemma I wanted originally, but of course it can trivially be deduced from mk_real_Ioo that's now there.)

[jcommelin]

LGTM

[fpvandoorn]

Just a tip, I don't care if you change it in this PR:
I personally tend to always avoid ▸; it's a weaker version of rw, and in some cases more brittle (although that is also me as a Lean 2 user talking; since the behavior of ▸ was a lot more unpredictable in Lean 2, and proofs could easily break with sequences of these substitutions).
In this case I think you can do:

refine le_antisymm _ _, { rw mk_real, exact mk_set_le _ }

I don't mind if you don't change it in this PR: I don't think it's an actual style guide, and all use cases are single line proof terms in this PR.

[fpvandoorn]

bors d+

feel free to merge this after the name changes.

Thanks for changing this to actual cardinal computations!

[bors]

✌️ jsm28 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[jsm28]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Lint mathlib
• Build mathlib
• Run tests and docs