Intervals without endpoints ordering #
In any decidable linear order α, we define the set of elements lying between two elements a and
b as Icc (min a b) (max a b).
Icc a b requires the assumption a ≤ b to be meaningful, which is sometimes inconvenient. The
interval as defined in this file is always the set of things lying between a and b, regardless
of the relative order of a and b.
For real numbers, Icc (min a b) (max a b) is the same as segment ℝ a b.
Notation #
We use the localized notation [a, b] for interval a b. One can open the locale interval to
make the notation available.
interval a b is the set of elements lying between a and b, with a and b included.
Equations
- set.interval a b = set.Icc (linear_order.min a b) (linear_order.max a b)
Instances for set.interval
@[simp]
theorem
set.interval_of_le
{α : Type u}
[linear_order α]
{a b : α}
(h : a ≤ b) :
set.interval a b = set.Icc a b
@[simp]
theorem
set.interval_of_ge
{α : Type u}
[linear_order α]
{a b : α}
(h : b ≤ a) :
set.interval a b = set.Icc b a
theorem
set.interval_swap
{α : Type u}
[linear_order α]
(a b : α) :
set.interval a b = set.interval b a
theorem
set.interval_of_lt
{α : Type u}
[linear_order α]
{a b : α}
(h : a < b) :
set.interval a b = set.Icc a b
theorem
set.interval_of_gt
{α : Type u}
[linear_order α]
{a b : α}
(h : b < a) :
set.interval a b = set.Icc b a
theorem
set.interval_of_not_le
{α : Type u}
[linear_order α]
{a b : α}
(h : ¬a ≤ b) :
set.interval a b = set.Icc b a
theorem
set.interval_of_not_ge
{α : Type u}
[linear_order α]
{a b : α}
(h : ¬b ≤ a) :
set.interval a b = set.Icc a b
@[simp]
@[simp]
@[simp]
@[simp]
theorem
set.Icc_subset_interval
{α : Type u}
[linear_order α]
{a b : α} :
set.Icc a b ⊆ set.interval a b
theorem
set.Icc_subset_interval'
{α : Type u}
[linear_order α]
{a b : α} :
set.Icc b a ⊆ set.interval a b
theorem
set.mem_interval_of_le
{α : Type u}
[linear_order α]
{a b x : α}
(ha : a ≤ x)
(hb : x ≤ b) :
x ∈ set.interval a b
theorem
set.mem_interval_of_ge
{α : Type u}
[linear_order α]
{a b x : α}
(hb : b ≤ x)
(ha : x ≤ a) :
x ∈ set.interval a b
theorem
set.not_mem_interval_of_lt
{α : Type u}
[linear_order α]
{a b c : α}
(ha : c < a)
(hb : c < b) :
c ∉ set.interval a b
theorem
set.not_mem_interval_of_gt
{α : Type u}
[linear_order α]
{a b c : α}
(ha : a < c)
(hb : b < c) :
c ∉ set.interval a b
theorem
set.interval_subset_interval
{α : Type u}
[linear_order α]
{a₁ a₂ b₁ b₂ : α}
(h₁ : a₁ ∈ set.interval a₂ b₂)
(h₂ : b₁ ∈ set.interval a₂ b₂) :
set.interval a₁ b₁ ⊆ set.interval a₂ b₂
theorem
set.interval_subset_Icc
{α : Type u}
[linear_order α]
{a₁ a₂ b₁ b₂ : α}
(ha : a₁ ∈ set.Icc a₂ b₂)
(hb : b₁ ∈ set.Icc a₂ b₂) :
set.interval a₁ b₁ ⊆ set.Icc a₂ b₂
theorem
set.interval_subset_interval_iff_mem
{α : Type u}
[linear_order α]
{a₁ a₂ b₁ b₂ : α} :
set.interval a₁ b₁ ⊆ set.interval a₂ b₂ ↔ a₁ ∈ set.interval a₂ b₂ ∧ b₁ ∈ set.interval a₂ b₂
theorem
set.interval_subset_interval_iff_le
{α : Type u}
[linear_order α]
{a₁ a₂ b₁ b₂ : α} :
set.interval a₁ b₁ ⊆ set.interval a₂ b₂ ↔ linear_order.min a₂ b₂ ≤ linear_order.min a₁ b₁ ∧ linear_order.max a₁ b₁ ≤ linear_order.max a₂ b₂
theorem
set.interval_subset_interval_right
{α : Type u}
[linear_order α]
{a b x : α}
(h : x ∈ set.interval a b) :
set.interval x b ⊆ set.interval a b
theorem
set.interval_subset_interval_left
{α : Type u}
[linear_order α]
{a b x : α}
(h : x ∈ set.interval a b) :
set.interval a x ⊆ set.interval a b
theorem
set.interval_subset_interval_union_interval
{α : Type u}
[linear_order α]
{a b c : α} :
set.interval a c ⊆ set.interval a b ∪ set.interval b c
A sort of triangle inequality.
The open-closed interval with unordered bounds.
Equations
- set.interval_oc = λ (a b : α), set.Ioc (linear_order.min a b) (linear_order.max a b)
Instances for set.interval_oc
theorem
set.interval_oc_of_le
{α : Type u}
[linear_order α]
{a b : α}
(h : a ≤ b) :
set.interval_oc a b = set.Ioc a b
theorem
set.interval_oc_of_lt
{α : Type u}
[linear_order α]
{a b : α}
(h : b < a) :
set.interval_oc a b = set.Ioc b a
theorem
set.interval_oc_eq_union
{α : Type u}
[linear_order α]
{a b : α} :
set.interval_oc a b = set.Ioc a b ∪ set.Ioc b a
theorem
set.interval_oc_subset_interval_oc_of_interval_subset_interval
{α : Type u}
[linear_order α]
{a b c d : α}
(h : set.interval a b ⊆ set.interval c d) :
set.interval_oc a b ⊆ set.interval_oc c d
theorem
set.interval_oc_swap
{α : Type u}
[linear_order α]
(a b : α) :
set.interval_oc a b = set.interval_oc b a
theorem
set.Ioc_subset_interval_oc
{α : Type u}
[linear_order α]
{a b : α} :
set.Ioc a b ⊆ set.interval_oc a b
theorem
set.Ioc_subset_interval_oc'
{α : Type u}
[linear_order α]
{a b : α} :
set.Ioc a b ⊆ set.interval_oc b a
@[simp]
theorem
set.preimage_const_add_interval
{α : Type u}
[linear_ordered_add_comm_group α]
(a b c : α) :
(λ (x : α), a + x) ⁻¹' set.interval b c = set.interval (b - a) (c - a)
@[simp]
theorem
set.preimage_add_const_interval
{α : Type u}
[linear_ordered_add_comm_group α]
(a b c : α) :
(λ (x : α), x + a) ⁻¹' set.interval b c = set.interval (b - a) (c - a)
@[simp]
theorem
set.preimage_neg_interval
{α : Type u}
[linear_ordered_add_comm_group α]
(a b : α) :
-set.interval a b = set.interval (-a) (-b)
@[simp]
theorem
set.preimage_sub_const_interval
{α : Type u}
[linear_ordered_add_comm_group α]
(a b c : α) :
(λ (x : α), x - a) ⁻¹' set.interval b c = set.interval (b + a) (c + a)
@[simp]
theorem
set.preimage_const_sub_interval
{α : Type u}
[linear_ordered_add_comm_group α]
(a b c : α) :
(λ (x : α), a - x) ⁻¹' set.interval b c = set.interval (a - b) (a - c)
@[simp]
theorem
set.image_const_add_interval
{α : Type u}
[linear_ordered_add_comm_group α]
(a b c : α) :
(λ (x : α), a + x) '' set.interval b c = set.interval (a + b) (a + c)
@[simp]
theorem
set.image_add_const_interval
{α : Type u}
[linear_ordered_add_comm_group α]
(a b c : α) :
(λ (x : α), x + a) '' set.interval b c = set.interval (b + a) (c + a)
@[simp]
theorem
set.image_const_sub_interval
{α : Type u}
[linear_ordered_add_comm_group α]
(a b c : α) :
(λ (x : α), a - x) '' set.interval b c = set.interval (a - b) (a - c)
@[simp]
theorem
set.image_sub_const_interval
{α : Type u}
[linear_ordered_add_comm_group α]
(a b c : α) :
(λ (x : α), x - a) '' set.interval b c = set.interval (b - a) (c - a)
theorem
set.image_neg_interval
{α : Type u}
[linear_ordered_add_comm_group α]
(a b : α) :
has_neg.neg '' set.interval a b = set.interval (-a) (-b)
theorem
set.abs_sub_le_of_subinterval
{α : Type u}
[linear_ordered_add_comm_group α]
{a b x y : α}
(h : set.interval x y ⊆ set.interval a b) :
If [x, y] is a subinterval of [a, b], then the distance between x and y
is less than or equal to that of a and b
theorem
set.abs_sub_left_of_mem_interval
{α : Type u}
[linear_ordered_add_comm_group α]
{a b x : α}
(h : x ∈ set.interval a b) :
If x ∈ [a, b], then the distance between a and x is less than or equal to
that of a and b
theorem
set.abs_sub_right_of_mem_interval
{α : Type u}
[linear_ordered_add_comm_group α]
{a b x : α}
(h : x ∈ set.interval a b) :
If x ∈ [a, b], then the distance between x and b is less than or equal to
that of a and b
@[simp]
theorem
set.preimage_mul_const_interval
{k : Type u}
[linear_ordered_field k]
{a : k}
(ha : a ≠ 0)
(b c : k) :
(λ (x : k), x * a) ⁻¹' set.interval b c = set.interval (b / a) (c / a)
@[simp]
theorem
set.preimage_const_mul_interval
{k : Type u}
[linear_ordered_field k]
{a : k}
(ha : a ≠ 0)
(b c : k) :
(λ (x : k), a * x) ⁻¹' set.interval b c = set.interval (b / a) (c / a)
@[simp]
theorem
set.preimage_div_const_interval
{k : Type u}
[linear_ordered_field k]
{a : k}
(ha : a ≠ 0)
(b c : k) :
(λ (x : k), x / a) ⁻¹' set.interval b c = set.interval (b * a) (c * a)
@[simp]
theorem
set.image_mul_const_interval
{k : Type u}
[linear_ordered_field k]
(a b c : k) :
(λ (x : k), x * a) '' set.interval b c = set.interval (b * a) (c * a)
@[simp]
theorem
set.image_const_mul_interval
{k : Type u}
[linear_ordered_field k]
(a b c : k) :
(λ (x : k), a * x) '' set.interval b c = set.interval (a * b) (a * c)
@[simp]
theorem
set.image_div_const_interval
{k : Type u}
[linear_ordered_field k]
(a b c : k) :
(λ (x : k), x / a) '' set.interval b c = set.interval (b / a) (c / a)