mathlib documentation

data.set.intervals.disjoint

Extra lemmas about intervals

This file contains lemmas about intervals that cannot be included into data.set.intervals.basic because this would create an import cycle. Namely, lemmas in this file can use definitions from data.set.lattice, including disjoint.

@[simp]
theorem set.Iic_disjoint_Ioi {α : Type u} [preorder α] {a b : α} :
a bdisjoint (set.Iic a) (set.Ioi b)

@[simp]
theorem set.Iic_disjoint_Ioc {α : Type u} [preorder α] {a b c : α} :
a bdisjoint (set.Iic a) (set.Ioc b c)

@[simp]
theorem set.Ioc_disjoint_Ioc_same {α : Type u} [preorder α] {a b c : α} :

@[simp]
theorem set.Ico_disjoint_Ico_same {α : Type u} [preorder α] {a b c : α} :

@[simp]
theorem set.Ico_disjoint_Ico {α : Type u} [linear_order α] {a₁ a₂ b₁ b₂ : α} :
disjoint (set.Ico a₁ a₂) (set.Ico b₁ b₂) min a₂ b₂ max a₁ b₁

@[simp]
theorem set.Ioc_disjoint_Ioc {α : Type u} [linear_order α] {a₁ a₂ b₁ b₂ : α} :
disjoint (set.Ioc a₁ a₂) (set.Ioc b₁ b₂) min a₂ b₂ max a₁ b₁

theorem set.eq_of_Ico_disjoint {α : Type u} [linear_order α] {x₁ x₂ y₁ y₂ : α} :
disjoint (set.Ico x₁ x₂) (set.Ico y₁ y₂)x₁ < x₂x₂ set.Ico y₁ y₂y₁ = x₂

If two half-open intervals are disjoint and the endpoint of one lies in the other, then it must be equal to the endpoint of the other.