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
order.locally_finite
.
TODO #
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 Icc
, Ioc
, 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.
Alias of the reverse direction of finset.Icc_eq_empty_iff
.
Alias of the reverse direction of finset.Ico_eq_empty_iff
.
Alias of the reverse direction of finset.Ioc_eq_empty_iff
.
A set with upper and lower bounds in a locally finite order is a fintype
Equations
- set.fintype_of_mem_bounds ha hb = (set.Icc a b).fintype_subset _
finset.cons
version of finset.Ico_insert_right
.
finset.cons
version of finset.Ioc_insert_left
.
finset.cons
version of finset.Ioo_insert_right
.
finset.cons
version of finset.Ioo_insert_left
.
finset.cons
version of finset.Ioi_insert
.
finset.cons
version of finset.Iio_insert
.
A sort of triangle inequality.