Intervals over linear orders

This file defines closed/open intervals over a linear order and the operations needed to build the interval-union semiring.

Main definitions

• Endpoint α – an endpoint of an interval: a value in α together with a closed flag indicating whether the endpoint is included
• Interval α – an interval with possibly open endpoints whose endpoints satisfy lo.val < hi.val, or lo.val = hi.val with both endpoints closed
• Interval.toSet – the set of points belonging to an interval
• Interval.disjoint – two intervals are disjoint when their point sets are disjoint
• Interval.before – I.before J means I lies strictly to the left of J (no point is shared and they cannot be merged)
• Interval.inter – intersection of two intervals
• Interval.diff – difference of two intervals (a list of at most two intervals)

Main results

• Interval.toSet_not_empty – every well-formed interval contains at least one point
• Interval.ext_toSet – two intervals with the same point set are equal (requires DenselyOrdered)
• Interval.mem_inter – membership in the intersection is conjunction of memberships
• Interval.mem_diff – membership in the difference is membership minus exclusion
• Interval.disjoint_of_before – before implies disjoint

structure Endpoint (α : Type) : Type

An endpoint of an interval: a value together with a boolean flag indicating whether the endpoint is included (closed = true) or excluded (closed = false).

• val : α
• closed : Bool

theorem Endpoint.ext {α : Type} {x y : Endpoint α} (val : x.val = y.val) (closed : x.closed = y.closed) : x = y

theorem Endpoint.ext_iff {α : Type} {x y : Endpoint α} : x = y ↔ x.val = y.val ∧ x.closed = y.closed

@[implicit_reducible]

instance Endpoint.instDecidableEq {α : Type} [DecidableEq α] : DecidableEq (Endpoint α)

Equations

• One or more equations did not get rendered due to their size.

def Endpoint.minLo {α : Type} [LinearOrder α] (a b : Endpoint α) : Endpoint α

Equations

• a.minLo b = if a.val < b.val then a else if b.val < a.val then b else if ¬a.closed = true ∧ b.closed = true then b else a

theorem Endpoint.minLo_or {α : Type} [LinearOrder α] (a b : Endpoint α) : a.minLo b = a ∨ a.minLo b = b

theorem Endpoint.minLo_commutative {α : Type} [LinearOrder α] {a b : Endpoint α} : a.minLo b = b.minLo a

theorem Endpoint.minLo_le_left {α : Type} [LinearOrder α] {a b : Endpoint α} : (a.minLo b).val ≤ a.val

def Endpoint.maxHi {α : Type} [LinearOrder α] (a b : Endpoint α) : Endpoint α

Equations

• a.maxHi b = if a.val > b.val then a else if b.val > a.val then b else if ¬a.closed = true ∧ b.closed = true then b else a

theorem Endpoint.maxHi_or {α : Type} [LinearOrder α] (a b : Endpoint α) : a.maxHi b = a ∨ a.maxHi b = b

theorem Endpoint.maxHi_commutative {α : Type} [LinearOrder α] {a b : Endpoint α} : a.maxHi b = b.maxHi a

theorem Endpoint.le_maxHi_left {α : Type} [LinearOrder α] {a b : Endpoint α} : a.val ≤ (a.maxHi b).val

def Endpoint.below {α : Type} [LinearOrder α] (x : α) (hi : Endpoint α) : Prop

below x hi holds when x is on the correct side of the upper endpoint hi, respecting its closedness: x ≤ hi.val if closed, x < hi.val if open.

Equations

• Endpoint.below x hi = if hi.closed = true then x ≤ hi.val else x < hi.val

def Endpoint.above {α : Type} [LinearOrder α] (x : α) (lo : Endpoint α) : Prop

above x lo holds when x is on the correct side of the lower endpoint lo, respecting its closedness: lo.val ≤ x if closed, lo.val < x if open.

Equations

• Endpoint.above x lo = if lo.closed = true then lo.val ≤ x else lo.val < x

theorem Endpoint.le_of_below {α : Type} [LinearOrder α] (x : α) (lo : Endpoint α) : below x lo → x ≤ lo.val

theorem Endpoint.ge_of_above {α : Type} [LinearOrder α] (x : α) (hi : Endpoint α) : above x hi → x ≥ hi.val

theorem Endpoint.below_of_below_of_lt {α : Type} [LinearOrder α] {hi hi' : Endpoint α} (h : hi.val < hi'.val) {x : α} : below x hi → below x hi'

theorem Endpoint.below_of_below_of_le {α : Type} [LinearOrder α] {hi hi' : Endpoint α} (h : hi.val ≤ hi'.val) (hep : ¬hi.closed = true ∨ hi'.closed = true) {x : α} : below x hi → below x hi'

theorem Endpoint.above_of_above_of_lt {α : Type} [LinearOrder α] {lo lo' : Endpoint α} (h : lo'.val < lo.val) {x : α} : above x lo → above x lo'

theorem Endpoint.above_of_above_of_le {α : Type} [LinearOrder α] {lo lo' : Endpoint α} (h : lo'.val ≤ lo.val) (hep : ¬lo.closed = true ∨ lo'.closed = true) {x : α} : above x lo → above x lo'

Endpoint operations for intersection and difference

def Endpoint.maxLo {α : Type} [LinearOrder α] (a b : Endpoint α) : Endpoint α

Most restrictive (largest) lower endpoint: above x (maxLo a b) ↔ above x a ∧ above x b.

Equations

• a.maxLo b = if b.val < a.val then a else if a.val < b.val then b else if a.closed = true ∧ ¬b.closed = true then b else a

def Endpoint.minHi {α : Type} [LinearOrder α] (a b : Endpoint α) : Endpoint α

Most restrictive (smallest) upper endpoint: below x (minHi a b) ↔ below x a ∧ below x b.

Equations

• a.minHi b = if a.val < b.val then a else if b.val < a.val then b else if a.closed = true ∧ ¬b.closed = true then b else a

theorem Endpoint.above_maxLo {α : Type} [LinearOrder α] (x : α) (a b : Endpoint α) : above x (a.maxLo b) ↔ above x a ∧ above x b

theorem Endpoint.below_minHi {α : Type} [LinearOrder α] (x : α) (a b : Endpoint α) : below x (a.minHi b) ↔ below x a ∧ below x b

structure Interval (α : Type) [LinearOrder α] : Type

An interval over a linear order, given by a lower endpoint lo and an upper endpoint hi satisfying lo.val < hi.val (strict) or lo.val = hi.val with both endpoints closed (degenerate point interval).

• lo : Endpoint α
• hi : Endpoint α
• wf : self.lo.val < self.hi.val ∨ self.lo.val = self.hi.val ∧ self.lo.closed = true ∧ self.hi.closed = true

theorem Interval.ext_iff {α : Type} {inst✝ : LinearOrder α} {x y : Interval α} : x = y ↔ x.lo = y.lo ∧ x.hi = y.hi

theorem Interval.ext {α : Type} {inst✝ : LinearOrder α} {x y : Interval α} (lo : x.lo = y.lo) (hi : x.hi = y.hi) : x = y

@[simp]

theorem Interval.le_lo_hi {α : Type} [LinearOrder α] (I : Interval α) : I.lo.val ≤ I.hi.val

@[simp]

theorem Interval.lo_below_hi {α : Type} [LinearOrder α] (I : Interval α) : Endpoint.below I.lo.val I.hi

@[simp]

theorem Interval.hi_above_lo {α : Type} [LinearOrder α] (I : Interval α) : Endpoint.above I.hi.val I.lo

def Interval.toSet {α : Type} [LinearOrder α] (I : Interval α) : Set α

The set of points belonging to an interval: those x that are above lo and below hi according to their respective closedness flags.

Equations

• I.toSet = {x : α | Endpoint.above x I.lo ∧ Endpoint.below x I.hi}

theorem Interval.eq_closed_lo {α : Type} [LinearOrder α] [DenselyOrdered α] {I J : Interval α} (h : I.toSet = J.toSet) : I.lo.closed = true → J.lo.closed = true

theorem Interval.eq_closed_hi {α : Type} [LinearOrder α] [DenselyOrdered α] {I J : Interval α} (h : I.toSet = J.toSet) : I.hi.closed = true → J.hi.closed = true

theorem Interval.eq_closed {α : Type} [LinearOrder α] [DenselyOrdered α] {I J : Interval α} (h : I.toSet = J.toSet) : I.lo.closed = J.lo.closed ∧ I.hi.closed = J.hi.closed

theorem Interval.toSet_not_empty {α : Type} [LinearOrder α] [DenselyOrdered α] (I : Interval α) : ∃ (x : α), x ∈ I.toSet

theorem Interval.ext_toSet {α : Type} [LinearOrder α] [DenselyOrdered α] {I J : Interval α} (h : I.toSet = J.toSet) : I = J

theorem Interval.ext_toSet_iff {α : Type} [LinearOrder α] [DenselyOrdered α] {I J : Interval α} : I = J ↔ I.toSet = J.toSet

@[simp]

theorem Interval.mem {α : Type} [LinearOrder α] (x : α) (I : Interval α) : x ∈ I.toSet ↔ Endpoint.above x I.lo ∧ Endpoint.below x I.hi

def Interval.disjoint {α : Type} [LinearOrder α] (I J : Interval α) : Prop

Two intervals are disjoint when their point sets have empty intersection.

Equations

• I.disjoint J = Disjoint I.toSet J.toSet

theorem Interval.not_mem_of_disjoint_right {α : Type} [LinearOrder α] {I J : Interval α} (h : I.disjoint J) (x : α) : x ∈ J.toSet → x ∉ I.toSet

@[implicit_reducible]

instance Interval.instPartialOrder {α : Type} [LinearOrder α] : PartialOrder (Interval α)

Equations

• One or more equations did not get rendered due to their size.

def Interval.before {α : Type} [LinearOrder α] (I J : Interval α) : Prop

I.before J means the intervals are strictly separated and cannot be merged: either I.hi.val < J.lo.val, or the endpoints meet at the same value but both are open.

Equations

• I.before J = (I.hi.val < J.lo.val ∨ I.hi.val = J.lo.val ∧ ¬I.hi.closed = true ∧ ¬J.lo.closed = true)

theorem Interval.disjoint_of_before {α : Type} [LinearOrder α] {I J : Interval α} : I.before J → I.disjoint J

@[implicit_reducible]

instance Interval.instDecidableBeforeOfDecidableEqOfDecidableLE {α : Type} [LinearOrder α] [DecidableEq α] [DecidableLE α] {I J : Interval α} : Decidable (I.before J)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Interval.le_of_before {α : Type} [LinearOrder α] {I J : Interval α} (h : I.before J) : I ≤ J

theorem Interval.before_of_before_of_le {α : Type} [LinearOrder α] {I J K : Interval α} (hIJ : I.before J) (hJK : J ≤ K) : I.before K

Interval intersection

def Interval.inter {α : Type} [LinearOrder α] (I J : Interval α) : List (Interval α)

Intersection of two intervals: empty or a single interval.

Equations

• One or more equations did not get rendered due to their size.

theorem Interval.mem_inter {α : Type} [LinearOrder α] (I J : Interval α) (x : α) : (∃ K ∈ I.inter J, x ∈ K.toSet) ↔ x ∈ I.toSet ∧ x ∈ J.toSet

Interval difference

theorem Interval.Endpoint.above_iff_not_below_complement {α : Type} [LinearOrder α] (x : α) (e : Endpoint α) : Endpoint.above x e ↔ ¬Endpoint.below x { val := e.val, closed := !e.closed }

above x e is the negation of below x at the complemented endpoint.

theorem Interval.Endpoint.below_iff_not_above_complement {α : Type} [LinearOrder α] (x : α) (e : Endpoint α) : Endpoint.below x e ↔ ¬Endpoint.above x { val := e.val, closed := !e.closed }

below x e is the negation of above x at the complemented endpoint.

def Interval.diff {α : Type} [LinearOrder α] (I J : Interval α) : List (Interval α)

Difference I \ J: the left piece (below J) and right piece (above J) of I.

Equations

• One or more equations did not get rendered due to their size.

theorem Interval.mem_diff {α : Type} [LinearOrder α] (I J : Interval α) (x : α) : (∃ K ∈ I.diff J, x ∈ K.toSet) ↔ x ∈ I.toSet ∧ x ∉ J.toSet

Home · Documentation · Publications · Contributors · Source · Cite