Intervals as finsets #
This file provides basic results about all the Finset.Ixx
, which are defined in
Order.LocallyFinite
.
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.fintypeOfMemBounds ha hb = Set.fintypeSubset (Set.Icc a b) (_ : ∀ (x : α), x ∈ s → a ≤ x ∧ x ≤ b)
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.