Set.eq_of_Ico_disjoint
theorem Set.eq_of_Ico_disjoint :
∀ {α : Type v} [inst : LinearOrder α] {x₁ x₂ y₁ y₂ : α},
Disjoint (Set.Ico x₁ x₂) (Set.Ico y₁ y₂) → x₁ < x₂ → x₂ ∈ Set.Ico y₁ y₂ → y₁ = x₂
The theorem `Set.eq_of_Ico_disjoint` states that for any type `α` with a linear order, given four elements `x₁`, `x₂`, `y₁`, and `y₂` of this type, if the half-open intervals from `x₁` to `x₂` and from `y₁` to `y₂` are disjoint, and if `x₁` is strictly less than `x₂` with `x₂` lying in the interval from `y₁` to `y₂`, then `y₁` must be equal to `x₂`. In other words, if the endpoint of one half-open interval lies in another disjoint half-open interval, then this endpoint must coincide with the starting point of the second interval.
More concisely: If `x₁ < x₂` are elements of a linearly ordered type with `x₂` in the interval `[y₁, y₂)` and the intervals `[x₁, x₂)` and `[y₁, y₂)` are disjoint, then `y₁ = x₂`.
|
IsGLB.biUnion_Ioi_eq
theorem IsGLB.biUnion_Ioi_eq :
∀ {α : Type v} [inst : LinearOrder α] {s : Set α} {a : α}, IsGLB s a → ⋃ x ∈ s, Set.Ioi x = Set.Ioi a
This theorem states that for any type `α` that has a linear order structure, and for any set `s` of elements of type `α` and any element `a` of the same type, if `a` is a greatest lower bound of set `s`, then the union of all open intervals greater than each element `x` in the set `s` is equivalent to the open interval of all elements greater than `a`. In mathematical notation, for all `x` in `s`, the union of `(x, ∞)` equals to `(a, ∞)` if `a` is the greatest lower bound of `s`.
More concisely: For any linearly ordered type `α` and set `s` of elements from `α` with greatest lower bound `a`, the union of all open intervals `(x, ∞)` for `x` in `s` equals the open interval `(a, ∞)`.
|
Set.Iic_disjoint_Ioi
theorem Set.Iic_disjoint_Ioi : ∀ {α : Type v} [inst : Preorder α] {a b : α}, a ≤ b → Disjoint (Set.Iic a) (Set.Ioi b)
This theorem states that for any type `α` that has a preorder, and for any two elements `a` and `b` of this type, if `a` is less than or equal to `b`, then the left-infinite right-closed interval ending at `a` (denoted as `Set.Iic a`) is disjoint with the left-open right-infinite interval starting after `b` (denoted as `Set.Ioi b`). In the context of this theorem, two sets are considered disjoint if their greatest lower bound (infimum) is the least element possible in the structure (`⊥`).
More concisely: For any preordered type `α`, elements `a` and `b` in `α` with `a ≤ b` imply `Set.Iic a` and `Set.Ioi b` are disjoint, that is, their infimum is the bottom element `⊥`.
|