Commit 2020-07-02 19:38 d84c48c8
View on Github →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).)