mathlib

d84c48c8 - feat(data/real/cardinality): cardinalities of intervals of reals (#3252)

feat(data/real/cardinality): cardinalities of intervals of reals (#3252) 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).)