Relations between intervals

This file defines the relations between two nonempty intervals of an ordered type that mathlib's NonemptyInterval API leaves implicit, and their counterparts on Interval, the intervals with a null element. Two intervals overlap when neither lies strictly beyond the other, i₁ precedes i₂ when it ends strictly before i₂ starts, and IsBefore lets the endpoints touch. During and FinalSubinterval refine containment, and IsPoint singles out the intervals with a single element. In a linear order two intervals occupy exactly one of three positions, precedence either way or overlap, and position records which as an Ordering, so that on point intervals it is compare.

Containment, the subinterval order and point intervals are mathlib's own (t ∈ i, i₁ ≤ i₂, pure t); lt_def unfolds strict containment to endpoints. On Interval α, where ≤ is inclusion and ⊓ intersection, Interval.Precedes is precedence stated pointwise, a left endpoint is IsLeast of the coerced set, NonemptyInterval.withTop embeds a bounded interval into WithTop α, and Interval.Ici a is the ray [a, ⊤].

Main definitions

• NonemptyInterval.Overlaps, NonemptyInterval.Precedes, NonemptyInterval.IsBefore: the order of two intervals.
• NonemptyInterval.During, NonemptyInterval.FinalSubinterval: refinements of containment.
• NonemptyInterval.position: the position of two intervals in a linear order as an Ordering.
• Interval.Precedes, Interval.Ici: pointwise precedence and rays on intervals with a null element.

References

• [All83]

Relations between intervals

def NonemptyInterval.Overlaps {α : Type u_1} [LE α] (i₁ i₂ : NonemptyInterval α) : Prop

Two intervals overlap when neither lies strictly beyond the other.

Equations

• i₁.Overlaps i₂ = (i₁.toProd.1 ≤ i₂.toProd.2 ∧ i₂.toProd.1 ≤ i₁.toProd.2)

def NonemptyInterval.IsPoint {α : Type u_1} [LE α] (i : NonemptyInterval α) : Prop

An interval is a point when its endpoints coincide.

Equations

• i.IsPoint = (i.toProd.1 = i.toProd.2)

def NonemptyInterval.IsBefore {α : Type u_1} [LE α] (i₁ i₂ : NonemptyInterval α) : Prop

i₁ is before i₂ when i₁ ends at or before i₂ starts.

Equations

• i₁.IsBefore i₂ = (i₁.toProd.2 ≤ i₂.toProd.1)

def NonemptyInterval.FinalSubinterval {α : Type u_1} [LE α] (i₁ i₂ : NonemptyInterval α) : Prop

i₁ is a final subinterval of i₂ when it lies within i₂ and shares its right endpoint.

Equations

• i₁.FinalSubinterval i₂ = (i₁ ≤ i₂ ∧ i₁.toProd.2 = i₂.toProd.2)

@[instance_reducible]

instance NonemptyInterval.instDecidableOverlaps {α : Type u_1} [LE α] {i₁ i₂ : NonemptyInterval α} [DecidableLE α] : Decidable (i₁.Overlaps i₂)

Equations

• NonemptyInterval.instDecidableOverlaps = { decide := decide (i₁.toProd.1 ≤ i₂.toProd.2) && decide (i₂.toProd.1 ≤ i₁.toProd.2), reflects_decide := ⋯ }

@[instance_reducible]

instance NonemptyInterval.instDecidableIsPoint {α : Type u_1} [LE α] [DecidableEq α] {i : NonemptyInterval α} : Decidable i.IsPoint

Equations

• NonemptyInterval.instDecidableIsPoint = NonemptyInterval.instDecidableIsPoint._aux_1

@[instance_reducible]

instance NonemptyInterval.instDecidableIsBefore {α : Type u_1} [LE α] {i₁ i₂ : NonemptyInterval α} [DecidableLE α] : Decidable (i₁.IsBefore i₂)

Equations

• NonemptyInterval.instDecidableIsBefore = NonemptyInterval.instDecidableIsBefore._aux_1

@[instance_reducible]

instance NonemptyInterval.instDecidableFinalSubinterval {α : Type u_1} [LE α] {i₁ i₂ : NonemptyInterval α} [DecidableLE α] [DecidableEq α] : Decidable (i₁.FinalSubinterval i₂)

Equations

• NonemptyInterval.instDecidableFinalSubinterval = { decide := decide (i₁ ≤ i₂) && decide (i₁.toProd.2 = i₂.toProd.2), reflects_decide := ⋯ }

@[simp]

theorem NonemptyInterval.overlaps_refl {α : Type u_1} [LE α] (i : NonemptyInterval α) : i.Overlaps i

theorem NonemptyInterval.overlaps_symm {α : Type u_1} [LE α] {i₁ i₂ : NonemptyInterval α} (h : i₁.Overlaps i₂) : i₂.Overlaps i₁

theorem NonemptyInterval.overlaps_comm {α : Type u_1} [LE α] (i₁ i₂ : NonemptyInterval α) : i₁.Overlaps i₂ ↔ i₂.Overlaps i₁

@[instance_reducible]

instance NonemptyInterval.instDecidableMemOfDecidableLE_linglib {α : Type u_1} [Preorder α] {a : α} {s : NonemptyInterval α} [DecidableLE α] : Decidable (a ∈ s)

Equations

• NonemptyInterval.instDecidableMemOfDecidableLE_linglib = decidable_of_iff' (s.toProd.1 ≤ a ∧ a ≤ s.toProd.2) ⋯

@[instance_reducible]

instance NonemptyInterval.instDecidableLtOfDecidableLE_linglib {α : Type u_1} [Preorder α] {s t : NonemptyInterval α} [DecidableLE α] : Decidable (s < t)

Equations

• NonemptyInterval.instDecidableLtOfDecidableLE_linglib = decidable_of_iff' (s ≤ t ∧ ¬t ≤ s) ⋯

def NonemptyInterval.Precedes {α : Type u_1} [Preorder α] (i₁ i₂ : NonemptyInterval α) : Prop

i₁ precedes i₂ when i₁ ends strictly before i₂ starts.

Equations

• i₁.Precedes i₂ = (i₁.toProd.2 < i₂.toProd.1)

def NonemptyInterval.During {α : Type u_1} [Preorder α] (i₁ i₂ : NonemptyInterval α) : Prop

i₁ lies during i₂ when it is strictly inside i₂ on both sides.

Equations

• i₁.During i₂ = (i₂.toProd.1 < i₁.toProd.1 ∧ i₁.toProd.2 < i₂.toProd.2)

@[instance_reducible]

instance NonemptyInterval.instDecidablePrecedesOfDecidableLE {α : Type u_1} [Preorder α] {i₁ i₂ : NonemptyInterval α} [DecidableLE α] : Decidable (i₁.Precedes i₂)

Equations

• NonemptyInterval.instDecidablePrecedesOfDecidableLE = decidable_of_iff' (i₁.toProd.2 ≤ i₂.toProd.1 ∧ ¬i₂.toProd.1 ≤ i₁.toProd.2) ⋯

@[instance_reducible]

instance NonemptyInterval.instDecidableDuringOfDecidableLE {α : Type u_1} [Preorder α] {i₁ i₂ : NonemptyInterval α} [DecidableLE α] : Decidable (i₁.During i₂)

Equations

• NonemptyInterval.instDecidableDuringOfDecidableLE = instDecidableAnd

theorem NonemptyInterval.during_irrefl {α : Type u_1} [Preorder α] (i : NonemptyInterval α) : ¬i.During i

theorem NonemptyInterval.not_precedes_of_during {α : Type u_1} [Preorder α] {i₁ i₂ : NonemptyInterval α} (h : i₁.During i₂) : ¬i₁.Precedes i₂ ∧ ¬i₂.Precedes i₁

An interval during another neither precedes nor follows it.

@[simp]

theorem NonemptyInterval.finalSubinterval_refl {α : Type u_1} [Preorder α] (i : NonemptyInterval α) : i.FinalSubinterval i

theorem NonemptyInterval.overlaps_of_le {α : Type u_1} [Preorder α] {i₁ i₂ : NonemptyInterval α} (h : i₁ ≤ i₂) : i₁.Overlaps i₂

Subintervals overlap their containing intervals.

theorem NonemptyInterval.precedes_irrefl {α : Type u_1} [Preorder α] (i : NonemptyInterval α) : ¬i.Precedes i

theorem NonemptyInterval.precedes_asymm {α : Type u_1} [Preorder α] {i₁ i₂ : NonemptyInterval α} (h : i₁.Precedes i₂) : ¬i₂.Precedes i₁

theorem NonemptyInterval.precedes_trans {α : Type u_1} [Preorder α] {i₁ i₂ i₃ : NonemptyInterval α} (h₁₂ : i₁.Precedes i₂) (h₂₃ : i₂.Precedes i₃) : i₁.Precedes i₃

theorem NonemptyInterval.precedes_of_le_of_precedes {α : Type u_1} [Preorder α] {i₁ i₂ i₃ : NonemptyInterval α} (h₁ : i₁ ≤ i₂) (h₂ : i₂.Precedes i₃) : i₁.Precedes i₃

A subinterval of an interval preceding i₃ precedes i₃.

theorem NonemptyInterval.precedes_not_overlaps {α : Type u_1} [Preorder α] {i₁ i₂ : NonemptyInterval α} (h : i₁.Precedes i₂) : ¬i₁.Overlaps i₂

Precedence and overlap are mutually exclusive.

theorem NonemptyInterval.lt_def {α : Type u_1} [LinearOrder α] {i₁ i₂ : NonemptyInterval α} : i₁ < i₂ ↔ i₁ ≤ i₂ ∧ (i₂.toProd.1 < i₁.toProd.1 ∨ i₁.toProd.2 < i₂.toProd.2)

Strict containment unfolded to endpoints, i₁ ≤ i₂ with a strictly interior endpoint.

theorem NonemptyInterval.Overlaps.mono_left {α : Type u_1} [LinearOrder α] {i₁ i₂ i₁' : NonemptyInterval α} (h : i₁.Overlaps i₂) (hle : i₁ ≤ i₁') : i₁'.Overlaps i₂

An interval containing an overlapping interval overlaps.

theorem NonemptyInterval.overlaps_iff_not_precedes {α : Type u_1} [LinearOrder α] {i₁ i₂ : NonemptyInterval α} : i₁.Overlaps i₂ ↔ ¬i₁.Precedes i₂ ∧ ¬i₂.Precedes i₁

In a linear order two intervals overlap exactly when neither precedes the other.

Relative position

In a linear order two intervals stand in exactly one of three positions: the first precedes the second, the second precedes the first, or they overlap. position records which as an Ordering, so that a set of admissible positions is a Finset Ordering, as a set of admissible comparisons of points is; on point intervals it is compare.

def NonemptyInterval.position {α : Type u_1} [LinearOrder α] (i₁ i₂ : NonemptyInterval α) : Ordering

The position of i₁ relative to i₂ is lt when i₁ precedes i₂, gt when i₂ precedes i₁, and eq when the two overlap.

Equations

• i₁.position i₂ = if i₁.Precedes i₂ then Ordering.lt else if i₂.Precedes i₁ then Ordering.gt else Ordering.eq

@[simp]

theorem NonemptyInterval.position_eq_lt {α : Type u_1} [LinearOrder α] {i₁ i₂ : NonemptyInterval α} : i₁.position i₂ = Ordering.lt ↔ i₁.Precedes i₂

@[simp]

theorem NonemptyInterval.position_eq_gt {α : Type u_1} [LinearOrder α] {i₁ i₂ : NonemptyInterval α} : i₁.position i₂ = Ordering.gt ↔ i₂.Precedes i₁

@[simp]

theorem NonemptyInterval.position_eq_eq {α : Type u_1} [LinearOrder α] {i₁ i₂ : NonemptyInterval α} : i₁.position i₂ = Ordering.eq ↔ i₁.Overlaps i₂

@[simp]

theorem NonemptyInterval.position_self {α : Type u_1} [LinearOrder α] (i : NonemptyInterval α) : i.position i = Ordering.eq

@[simp]

theorem NonemptyInterval.position_pure {α : Type u_1} [LinearOrder α] (a b : α) : (pure a).position (pure b) = compare a b

On point intervals the position is the comparison of the points.

theorem NonemptyInterval.position_eq_eq_of_le {α : Type u_1} [LinearOrder α] {i₁ i₂ i₁' : NonemptyInterval α} (h : i₁.position i₂ = Ordering.eq) (hle : i₁ ≤ i₁') : i₁'.position i₂ = Ordering.eq

An interval containing one that overlaps i₂ overlaps i₂.

Embedding into WithTop

def NonemptyInterval.withTop {α : Type u_1} [Preorder α] (i : NonemptyInterval α) : NonemptyInterval (WithTop α)

An interval of α as an interval of WithTop α.

Equations

• i.withTop = NonemptyInterval.map WithTop.coeOrderHom.toOrderHom i

@[simp]

theorem NonemptyInterval.fst_withTop {α : Type u_1} [Preorder α] (i : NonemptyInterval α) : i.withTop.toProd.1 = ↑i.toProd.1

@[simp]

theorem NonemptyInterval.snd_withTop {α : Type u_1} [Preorder α] (i : NonemptyInterval α) : i.withTop.toProd.2 = ↑i.toProd.2

@[simp]

theorem NonemptyInterval.mem_withTop {α : Type u_1} [Preorder α] {i : NonemptyInterval α} {x : WithTop α} : x ∈ i.withTop ↔ ↑i.toProd.1 ≤ x ∧ x ≤ ↑i.toProd.2

@[simp]

theorem NonemptyInterval.withTop_le_withTop {α : Type u_1} [Preorder α] {i j : NonemptyInterval α} : i.withTop ≤ j.withTop ↔ i ≤ j

Intervals with a null element

def Interval.Precedes {α : Type u_1} [PartialOrder α] (s t : Interval α) : Prop

s precedes t when every element of s is below every element of t, Allen's before stated pointwise, vacuously so at the null interval.

Equations

• s.Precedes t = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ t → x < y

@[simp]

theorem Interval.notMem_bot {α : Type u_1} [PartialOrder α] {x : α} : x ∉ ⊥

theorem Interval.coe_le_iff {α : Type u_1} [PartialOrder α] {s : Interval α} {i : NonemptyInterval α} : ↑i ≤ s ↔ i.toProd.1 ∈ s ∧ i.toProd.2 ∈ s

A nonempty interval lies within s exactly when its endpoints do.

@[simp]

theorem Interval.pure_le_iff {α : Type u_1} [PartialOrder α] {s : Interval α} {a : α} : pure a ≤ s ↔ a ∈ s

theorem Interval.isLeast_coe_fst {α : Type u_1} [PartialOrder α] {i : NonemptyInterval α} : IsLeast (↑↑i) i.toProd.1

The left endpoint is the least element.

theorem Interval.precedes_coe_coe {α : Type u_1} [PartialOrder α] {i j : NonemptyInterval α} : (↑i).Precedes ↑j ↔ i.Precedes j

Nonempty intervals precede exactly when the one ends before the other starts, the endpoint form of the relation.

theorem Interval.not_disjoint_iff {α : Type u_1} [Lattice α] {s t : Interval α} : ¬Disjoint s t ↔ ∃ x ∈ s, x ∈ t

theorem Interval.not_disjoint_coe_coe {α : Type u_1} [Lattice α] {i j : NonemptyInterval α} : ¬Disjoint ↑i ↑j ↔ i.Overlaps j

Nonempty intervals meet exactly when they overlap, the endpoint form of the relation.

@[simp]

theorem Interval.mem_inf {α : Type u_1} [Lattice α] {s t : Interval α} {x : α} [DecidableLE α] : x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t

Rays

def Interval.Ici {α : Type u_1} [PartialOrder α] [OrderTop α] (a : α) : Interval α

The ray [a, ⊤].

Equations

• Interval.Ici a = ↑{ fst := a, snd := ⊤, fst_le_snd := ⋯ }

@[simp]

theorem Interval.mem_Ici {α : Type u_1} [PartialOrder α] [OrderTop α] {a x : α} : x ∈ Ici a ↔ a ≤ x

@[simp]

theorem Interval.Ici_le_Ici {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} : Ici a ≤ Ici b ↔ b ≤ a

theorem Interval.antitone_Ici {α : Type u_1} [PartialOrder α] [OrderTop α] : Antitone Ici

@[simp]

theorem Interval.pure_le_Ici {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} : pure b ≤ Ici a ↔ a ≤ b

theorem Interval.le_Ici_iff {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} {s : Interval α} : s ≤ Ici a ↔ ∀ x ∈ s, a ≤ x

An interval lies within the ray from a exactly when all its elements are at or above a.

theorem Interval.withTop_le_Ici {α : Type u_1} [PartialOrder α] {i : NonemptyInterval α} {a : α} : ↑i.withTop ≤ Ici ↑a ↔ a ≤ i.toProd.1

A bounded interval lies within the ray from a exactly when it starts at or above a.

theorem Interval.precedes_withTop_Ici {α : Type u_1} [PartialOrder α] {i : NonemptyInterval α} {a : α} : (↑i.withTop).Precedes (Ici ↑a) ↔ i.toProd.2 < a

A bounded interval precedes the ray from a exactly when it ends below a.

theorem Interval.precedes_withTop_pure {α : Type u_1} [PartialOrder α] {i : NonemptyInterval α} {a : α} : (↑i.withTop).Precedes (pure ↑a) ↔ i.toProd.2 < a

A bounded interval precedes the point a exactly when it ends below a.

theorem Interval.not_disjoint_withTop_Ici {α : Type u_1} [Lattice α] {i : NonemptyInterval α} {a : α} : ¬Disjoint (↑i.withTop) (Ici ↑a) ↔ a ≤ i.toProd.2

A bounded interval meets the ray from a exactly when it ends at or above a.