If α is a type with a LinearOrder, and c is some Cardinal in the same universe, then
IsEta c α states that for any two subsets X Y : Set α of cardinality less than c, if every
element of X is less than every element of Y, then there is some (z : α) greater than all
elements of X and less than all elements of Y.
In the literature, an η_o ordered set would be a IsEta ℵ_o order, but this definition is more
general.
Equations
- Order.IsEta c α = ∀ ⦃s t : Set α⦄, Cardinal.mk ↑s < c → Cardinal.mk ↑t < c → (∀ x ∈ s, ∀ y ∈ t, x < y) → ∃ (z : α), (∀ x ∈ s, x < z) ∧ ∀ y ∈ t, z < y
Instances For
IsEta is unchanged under the order dual.
theorem
Order.IsEta.exists_between
{α : Type u}
[LinearOrder α]
{c : Cardinal.{u}}
(h : IsEta c α)
{s t : Set α}
(hs : Cardinal.mk ↑s < c)
(ht : Cardinal.mk ↑t < c)
(hB : ∀ x ∈ s, ∀ y ∈ t, x < y)
:
theorem
Order.IsEta.mono
{α : Type u}
[LinearOrder α]
{c c' : Cardinal.{u}}
(h : IsEta c α)
(hc : c' ≤ c)
:
IsEta c' α
theorem
Order.IsEta.nonempty
{α : Type u}
[LinearOrder α]
{c : Cardinal.{u}}
(hc : c ≠ 0)
(h : IsEta c α)
:
Nonempty α
theorem
Order.IsEta.denselyOrdered
{α : Type u}
[LinearOrder α]
{c : Cardinal.{u}}
(hc : 1 < c)
(h : IsEta c α)
:
theorem
Order.IsEta.noMinOrder
{α : Type u}
[LinearOrder α]
{c : Cardinal.{u}}
(hc : 1 < c)
(h : IsEta c α)
:
theorem
Order.IsEta.noMaxOrder
{α : Type u}
[LinearOrder α]
{c : Cardinal.{u}}
(hc : 1 < c)
(h : IsEta c α)
:
theorem
Order.IsEta.infinite
{α : Type u}
[LinearOrder α]
{c : Cardinal.{u}}
(hc : 1 < c)
(h : IsEta c α)
[Nonempty α]
:
Infinite α
theorem
Order.IsEta.congr
{α β : Type u}
[LinearOrder α]
[LinearOrder β]
{c : Cardinal.{u}}
(e : α ≃o β)
:
Order-isomorphic linear orders satisfy IsEta for the same cardinal.
theorem
Order.IsEta.orderType_eq
{α β : Type u}
[LinearOrder α]
[LinearOrder β]
{c : Cardinal.{u}}
(h : OrderType.type α = OrderType.type β)
:
theorem
Order.IsEta.aleph0
{α : Type u}
[LinearOrder α]
[Nonempty α]
[DenselyOrdered α]
[NoMaxOrder α]
[NoMinOrder α]
: