Intervals as finsets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file provides basic results about all the
finset.Ixx, which are defined in
This file was originally only about
finset.Ico a b where
a b : ℕ. No care has yet been taken to
generalize these lemmas properly and many lemmas about
Ioo are missing. In general,
what's to do is taking the lemmas in
data.x.intervals and abstract away the concrete structure.
Complete the API. See https://github.com/leanprover-community/mathlib/pull/14448#discussion_r906109235 for some ideas.
A set with upper and lower bounds in a locally finite order is a fintype