Order.PartialIso.exists_across
theorem Order.PartialIso.exists_across :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] [inst_2 : DenselyOrdered β]
[inst_3 : NoMinOrder β] [inst_4 : NoMaxOrder β] [inst_5 : Nonempty β] (f : Order.PartialIso α β) (a : α),
∃ b, ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
This theorem, `Order.PartialIso.exists_across`, states that for every element `a` of a type `α`, under the conditions that `α` and `β` are linearly ordered, `β` is densely ordered, and `β` has neither a minimum nor a maximum element but is not empty, there exists an element `b` in type `β` such that the relation of `a` to the domain of a partial order isomorphism `f` is the same as the relation of `b` to the image of `f`. This means that if `a` is not already in `f`, we can extend `f` by mapping `a` to `b`.
More concisely: For every linearly ordered type `α` with densely ordered, non-empty, and bounded-but-not-empty image `β` under a partial order isomorphism `f`, there exists an element `b` in `β` such that `a` and `f(a)` have the same relation under `f` for all `a` in `α`.
|
Order.iso_of_countable_dense
theorem Order.iso_of_countable_dense :
∀ (α : Type u_1) (β : Type u_2) [inst : LinearOrder α] [inst_1 : LinearOrder β] [inst_2 : Countable α]
[inst_3 : DenselyOrdered α] [inst_4 : NoMinOrder α] [inst_5 : NoMaxOrder α] [inst_6 : Nonempty α]
[inst_7 : Countable β] [inst_8 : DenselyOrdered β] [inst_9 : NoMinOrder β] [inst_10 : NoMaxOrder β]
[inst_11 : Nonempty β], Nonempty (α ≃o β)
This theorem states that for any two types `α` and `β`, if both types are countable, densely ordered, have no minimum or maximum elements, and are nonempty, then there exists an order isomorphism between `α` and `β`. In other words, any two countable dense, nonempty linear orders without endpoints are order-isomorphic.
More concisely: If types `α` and `β` are countable, densely ordered, nonempty sets without minimum or maximum elements, then there exists an order isomorphism between `α` and `β`.
|
Order.embedding_from_countable_to_dense
theorem Order.embedding_from_countable_to_dense :
∀ (α : Type u_1) (β : Type u_2) [inst : LinearOrder α] [inst_1 : LinearOrder β] [inst_2 : Countable α]
[inst_3 : DenselyOrdered β] [inst_4 : Nontrivial β], Nonempty (α ↪o β)
This theorem states that for any two types `α` and `β`, if `α` is a countable linear order and `β` is a nontrivial dense linear order, then there exists an order-preserving embedding from `α` into `β`. In other words, we can map each element of `α` to an element of `β` in such a way that the order of elements is preserved, and every element of `α` corresponds to a unique element of `β`.
More concisely: Given countable linear orders `α` and nontrivial dense `β`, there exists an order-preserving embedding from `α` into `β`.
|
Order.exists_between_finsets
theorem Order.exists_between_finsets :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : NoMinOrder α] [inst_3 : NoMaxOrder α]
[nonem : Nonempty α] (lo hi : Finset α), (∀ x ∈ lo, ∀ y ∈ hi, x < y) → ∃ m, (∀ x ∈ lo, x < m) ∧ ∀ y ∈ hi, m < y
The theorem `Order.exists_between_finsets` asserts that if we have a nonempty, densely ordered set `α` without minimum or maximum elements, and two finite subsets `lo` and `hi` such that every element of `lo` is strictly less than every element of `hi`, then there exists an element `m` in `α` that is strictly greater than every element in `lo` and strictly less than every element in `hi`. Essentially, no matter how we choose `lo` and `hi`, we can always find an element in `α` that lies strictly between these two subsets.
More concisely: If `α` is a nonempty, densely ordered set without minimum or maximum elements, then for any finite subsets `lo` and `hi` such that every element of `lo` is strictly less than every element of `hi`, there exists an element `m` in `α` with `lo.min < m < hi.max`.
|