Set.ordConnected_Iio
theorem Set.ordConnected_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, (Set.Iio a).OrdConnected
This theorem states that for any type `α` with a preorder (`Preorder α`), and for any element `a` of type `α`, the left-infinite right-open interval up to 'a' (denoted as `Set.Iio a`) is ordered-connected. Ordered-connectedness means that for any two elements in the set, all elements between them (in the order) are also contained within the set. In other words, for any set of numbers, if we take two numbers from the set, all the numbers in between them also belong to the set.
More concisely: For any type `α` with a preorder and any element `a` in `α`, the left-infinite right-open interval `Set.Iio a` is ordered-connected, meaning any two elements in the interval have every element between them also in the interval.
|
Set.ordConnected_Ioo
theorem Set.ordConnected_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (Set.Ioo a b).OrdConnected
The theorem `Set.ordConnected_Ioo` states that for any type `α` that has a preorder relation, and any two elements `a` and `b` of this type, the open interval `(a, b)` (denoted as `Set.Ioo a b` in Lean) is order-connected. In terms of mathematics, this can be understood as: given any two points in the open interval `(a, b)`, all points between them (according to the preorder) are also in the interval.
More concisely: For any type `α` with a preorder relation and any `a < b` in `α`, the open interval `(a, b)` consists only of elements between `a` and `b` according to the preorder.
|
Set.ordConnected_Ioc
theorem Set.ordConnected_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (Set.Ioc a b).OrdConnected
This theorem states that for any type `α` that has a preorder structure, any left-open right-closed interval, denoted as `(a, b]` or `Set.Ioc a b` in Lean 4, is order-connected. In terms of mathematical language, an interval `(a, b]` in a preordered set is said to be order-connected if, for any two points `x` and `y` in `(a, b]` with `x ≤ y`, all points `z` in the set such that `x ≤ z ≤ y` are also in `(a, b]`.
More concisely: In a preordered set, any left-open right-closed interval is order-connected, meaning all elements x, y in the interval with x ≤ y imply that every z in the interval between x and y also satisfies x ≤ z ≤ y.
|
Set.ordConnected_Icc
theorem Set.ordConnected_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (Set.Icc a b).OrdConnected
This theorem states that for any type `α` with a preorder structure and any two elements `a` and `b` of that type, the left-closed right-closed interval `Set.Icc a b` is order-connected. In mathematical terms, this means that for every two points in the interval, every point in between them is also in the interval. The interval `Set.Icc a b` is defined as the set of all elements `x` which satisfy the condition `a ≤ x ∧ x ≤ b`.
More concisely: For any type `α` with a preorder structure and any two elements `a` and `b` of that type, the interval `Set.Icc a b` is order-connected, that is, for all `x, y` in `Set.Icc a b` with `x ≤ y`, there exists a sequence `x = z₀, z₁, ..., zₙ = y` in `Set.Icc a b` such that `z₀ ≤ z₁ ≤ ... ≤ zₙ`.
|
Set.ordConnected_Ici
theorem Set.ordConnected_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, (Set.Ici a).OrdConnected
This theorem states that for any type `α` with a preorder relation, and any element `a` of the type `α`, the set of all elements `x` such that `a ≤ x` (represented as `Set.Ici a`) is order-connected. In other words, for any two elements `b` and `c` in the set where `b ≤ c` , all elements `x` between `b` and `c` (inclusive) are also in the set.
More concisely: For any type `α` with a preorder relation and any element `a` in `α`, the set `{x : α | x ≤ a}` is order-connected.
|
Set.OrdConnected.out'
theorem Set.OrdConnected.out' :
∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [self : s.OrdConnected] ⦃x : α⦄,
x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.Icc x y ⊆ s
The theorem `Set.OrdConnected.out'` states that for a set `s` of some type `α` with a preordained structure, if `s` is order-connected, then for any two elements `x` and `y` in `s`, the closed interval from `x` to `y` (inclusive) is a subset of `s`. In other words, if `s` is order-connected, then it includes the entire interval between any two elements in the set.
More concisely: If `s` is an order-connected subset of type `α`, then for all `x, y ∈ s`, the interval `[x, y] ⊆ s`.
|
Set.ordConnected_Iic
theorem Set.ordConnected_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, (Set.Iic a).OrdConnected
This theorem states that for any type `α` that has a preorder relation, and any element `a` of type `α`, the left-infinite right-closed interval up to `a` (denoted as `Set.Iic a`) is order-connected. In mathematical terms, an interval is order-connected if, given any two elements in the interval, any element that is between these two elements is also in the interval. Here, the interval is defined as the set of all elements `x` of type `α` such that `x` is less than or equal to `a`.
More concisely: For any type `α` with a preorder relation and any element `a` in `α`, the left-infinite right-closed interval `{x : α | x ≤ a}` is order-connected.
|
Set.OrdConnected.inter
theorem Set.OrdConnected.inter :
∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, s.OrdConnected → t.OrdConnected → (s ∩ t).OrdConnected := by
sorry
This theorem states that for any type `α` that has a preorder relation, if `s` and `t` are two sets of `α` that are order-connected (meaning that for every pair of points in the set, every point between them is also in the set), then the intersection of `s` and `t` is also an order-connected set.
More concisely: If `s` and `t` are order-connected subsets of a preordered type `α`, then their intersection `s INTER t` is also an order-connected subset.
|
Set.OrdConnected.uIcc_subset
theorem Set.OrdConnected.uIcc_subset :
∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α},
s.OrdConnected → ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.uIcc x y ⊆ s
The theorem `Set.OrdConnected.uIcc_subset` states that for any type `α` with a linear order and any set `s` of `α` that is order-connected (meaning, for any two elements `a` and `b` in the set, if `a ≤ b`, then all elements `c` with `a ≤ c ≤ b` are also in the set), if `x` and `y` are elements in set `s`, then the set of all elements lying between `x` and `y` inclusive (denoted as `Set.uIcc x y`) is a subset of `s`. In other words, any continuous interval in an order-connected set remains within that set.
More concisely: For any order-connected subset `s` of a linearly ordered type `α`, the interval `[x, y]` (or `{z : α | x ≤ z ≤ y}`) is contained in `s`, given `x, y ∈ s`.
|
Set.ordConnected_iff_uIcc_subset_left
theorem Set.ordConnected_iff_uIcc_subset_left :
∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α},
x ∈ s → (s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → Set.uIcc x y ⊆ s)
This theorem states that for any type `α` with a linear order, a set `s` of elements of type `α`, and an element `x` of type `α` that belongs to `s`, the set `s` is order-connected if and only if for any element `y` of type `α` that belongs to `s`, the set of elements between `x` and `y` (inclusive) is a subset of `s`. Here, order-connected means that for any two elements in the set, all the elements that lie between these two elements (inclusive) also belong to the set. The `Set.uIcc x y` function returns the set of elements lying between `x` and `y` (inclusive).
More concisely: For any linear order type `α`, set `s` of elements from `α`, and `x, y ∈ s`, if `s` is order-connected then `Set.uIcc x y ⊆ s`.
|
Set.ordConnected_iff
theorem Set.ordConnected_iff :
∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, s.OrdConnected ↔ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Set.Icc x y ⊆ s := by
sorry
This theorem states that for a given set `s` of type `α` (where `α` is a type with the Preorder relation), the set `s` is order-connected, i.e., for any two elements `x` and `y` in `s` such that `x` is less than or equal to `y`, if and only if the closed interval from `x` to `y`, denoted `Set.Icc x y`, is a subset of `s`. In other words, if each point `z` between `x` and `y` (inclusive) is also in `s`, then `s` is an order-connected set.
More concisely: A set `s` of type `α` with the Preorder relation is order-connected if and only if for all `x` and `y` in `s` with `x ≤ y`, the closed interval `[x, y]` (or `Set.Icc x y`) is a subset of `s`.
|
Set.ordConnected_Ioi
theorem Set.ordConnected_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, (Set.Ioi a).OrdConnected
The theorem `Set.ordConnected_Ioi` states that for any type `α` that has a preorder structure and for any element `a` of type `α`, the left-open right-infinite interval `(a, +∞)` denoted `Set.Ioi a` is order-connected. In the context of order theory, a set is said to be order-connected if for every pair of elements in the set where one is less than the other, all elements that lie between these two are also in the set. In this case, for any two elements in the set `Set.Ioi a` where one is less than the other, all elements that lie between them are also in `Set.Ioi a`.
More concisely: For any preordered type `α` and element `a` in `α`, the left-open right-infinite interval `(a, +∞)` in `α` is order-connected.
|
Set.OrdConnected.out
theorem Set.OrdConnected.out :
∀ {α : Type u_1} [inst : Preorder α] {s : Set α},
s.OrdConnected → ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.Icc x y ⊆ s
This theorem states that for any type `α` with a preorder relation, if a set `s` of type `α` is ordered-connected, then for any elements `x` and `y` in the set `s`, the closed interval from `x` to `y` (both `x` and `y` included) is a subset of `s`. In other words, if a set is ordered-connected, then every element between two elements of the set (inclusive) also belongs to the set.
More concisely: In a preordered type `α`, if `s` is an ordered-connected subset, then for all `x, y ∈ s`, the interval `[x, y] ⊆ s`.
|
Set.OrdConnected.preimage_mono
theorem Set.OrdConnected.preimage_mono :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : β → α},
s.OrdConnected → Monotone f → (f ⁻¹' s).OrdConnected
The theorem `Set.OrdConnected.preimage_mono` states that for all types `α` and `β` with preordering, if a set `s` of type `α` is order-connected and a function `f` from `β` to `α` is monotone, then the preimage of `s` under `f` (i.e., the set of all elements in `β` that `f` maps into `s`) is also order-connected.
In other words, if `s` is a set where for any two elements in it, all elements between them (in terms of the order) also belong to `s`, and if `f` is a function that preserves the order, then the set of elements that `f` maps into `s` also has this property of containing all elements between any two of its elements.
More concisely: If `s` is an order-connected subset of type `α` and `f` is a monotone function from type `β` to `α`, then `f⁻¹[s]` (the preimage of `s` under `f`) is also an order-connected subset of `β`.
|
Set.ordConnected_biInter
theorem Set.ordConnected_biInter :
∀ {α : Type u_1} [inst : Preorder α] {ι : Sort u_3} {p : ι → Prop} {s : (i : ι) → p i → Set α},
(∀ (i : ι) (hi : p i), (s i hi).OrdConnected) → (⋂ i, ⋂ (hi : p i), s i hi).OrdConnected
This theorem states that for any type `α` with a preorder relation, given an indexed collection of sets `{s i hi}` indexed by `ι` and filtered by a property `p`, if each of these sets is ordinally connected (i.e., any two elements in the set can be connected by a non-decreasing sequence), then their intersection is also ordinally connected. In other words, if each of the sets `{s i hi}` is such that for any two elements `a` and `b` in it with `a ≤ b`, all elements `c` with `a ≤ c ≤ b` are also in the set, then the same property holds for the intersection of all these sets.
More concisely: If each set in an indexed collection of ordinally connected sets filtered by a property satisfies the property that any two elements related by a preorder relation have all elements related by that preorder relation between them, then their intersection is also ordinally connected.
|
Set.ordConnected_iInter
theorem Set.ordConnected_iInter :
∀ {α : Type u_1} [inst : Preorder α] {ι : Sort u_3} {s : ι → Set α},
(∀ (i : ι), (s i).OrdConnected) → (⋂ i, s i).OrdConnected
This theorem states that for any type `α` with a preorder structure and any indexed collection `{s : ι → Set α}` of sets, if each set `s i` in this collection is order-connected (meaning for any two points in the set, all points between them are also in the set), then the intersection of all these sets (⋂ i, s i) is also order-connected. In other words, if every set in a collection is order-connected, their intersection retains this property.
More concisely: If each set in an indexed collection of order-connected sets in a preordered type intersects to form a non-empty set, then the resulting intersection is also order-connected.
|