subintervals

Stream: general

[Yury G. Kudryashov]

In #4913 I introduce a type called set.subinterval defined as

/-- A nonempty closed subinterval of set `α`. -/
@[ext] structure subinterval [preorder α] (s : set α) :=
(left right : α)
(nontrivial : left ≤ right)
(Icc_subset : set.Icc left right ⊆ s)

I'm not sure if bundling Icc_subset is a good idea. While it is convenient for the proofs in #4913 (I construct a decreasing sequence of subintervals, and it's convenient to automatically know that s includes all of them), this type is less reusable than, e.g.,

structure binterval (α : Type*) [preorder α] :=
(left right : α)
(nontrivial : left ≤ right)

with binterval.Ixx methods to access the underlying sets. What do you think?

Another option is to completely drop this type and deal with f : α → α → M instead of f : subinterval s → M.