Set.ordConnectedComponent_subset
theorem Set.ordConnectedComponent_subset :
∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α}, s.ordConnectedComponent x ⊆ s
This theorem states that for any given type `α` that has a linear order, any set `s` of type `α`, and any element `x` of type `α`, the order-connected component of `x` in `s` is a subset of `s`. In mathematical terms, if we consider a set `s` and a point `x` in a space with linear order, the set of all points `y` such that the interval from `x` to `y` is contained within `s` (this is the order-connected component of `x` in `s`) is always a subset of `s` itself.
More concisely: For any type `α` with a linear order, any set `s` of elements from `α`, and any `x` in `s`, the order-connected component of `x` in `s` is a subset of `s`.
|
Set.mem_ordConnectedComponent
theorem Set.mem_ordConnectedComponent :
∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x y : α}, y ∈ s.ordConnectedComponent x ↔ Set.uIcc x y ⊆ s
This theorem states that for any given type `α` with a linear order, any set `s` of type `α`, and any two elements `x` and `y` of type `α`, `y` is a member of the order-connected component of `x` in set `s` if and only if the set of elements lying between `x` and `y`, inclusive, is a subset of `s`. In other words, `y` is in the order-connected component of `x` if all elements between `x` and `y`, inclusive, are also in the set `s`.
More concisely: For a linear ordered type `α` and a subset `s` of `α`, an element `y` belongs to the order-connected component of `x` in `s` if and only if the interval [`x`, `y`] (inclusive) is a subset of `s`.
|
Set.ordConnectedProj.proof_1
theorem Set.ordConnectedProj.proof_1 :
∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α) (x : ↑s), (s.ordConnectedComponent ↑x).Nonempty
This theorem states that for any type `α` that has a linear order and for any set `s` of type `α`, if `x` is an element of this set `s`, then the order-connected component of `x` in `s` is non-empty. In other words, there exists at least one element `y` such that the set of all points between `x` and `y` (inclusive) is a subset of `s`.
More concisely: Given a type `α` with a linear order and a set `s` of `α`, for each `x` in `s`, there exists `y` in `s` such that the interval [`x`, `y`] is included in `s`.
|