Eta sets

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.

Every linear order is vacuously IsEta 0, and the IsEta 1 predicate is equivalent to Nonempty. For 1 < c ≤ ℵ₀, the predicate IsEta c is equivalent to DenselyOrdered. Examples of IsEta c orders for uncountable c include the surreals and the hyperreals.

In the literature, an η_o ordered set would be a IsEta ℵ_o order, but this definition is more general.

def Order.IsEta (c : Cardinal.{u}) (α : Type u) [LinearOrder α] : Prop

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.

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

theorem Order.IsEta.dual_iff {α : Type u} [LinearOrder α] {c : Cardinal.{u}} : IsEta c α ↔ IsEta c αᵒᵈ

IsEta is unchanged under the order dual.

theorem Order.IsEta.dual {α : Type u} [LinearOrder α] {c : Cardinal.{u}} : IsEta c αᵒᵈ → IsEta c α

Alias of the reverse direction of Order.IsEta.dual_iff.

---

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) : ∃ (z : α), (∀ x ∈ s, x < z) ∧ ∀ y ∈ t, z < y

theorem Order.IsEta.zero {α : Type u} [LinearOrder α] : IsEta 0 α

theorem Order.IsEta.mono {α : Type u} [LinearOrder α] {c c' : Cardinal.{u}} (h : IsEta c α) (hc : c' ≤ c) : IsEta c' α

theorem Order.IsEta.one {α : Type u} [LinearOrder α] [Nonempty α] : IsEta 1 α

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 α) : DenselyOrdered α

theorem Order.IsEta.noMinOrder {α : Type u} [LinearOrder α] {c : Cardinal.{u}} (hc : 1 < c) (h : IsEta c α) : NoMinOrder α

theorem Order.IsEta.noMaxOrder {α : Type u} [LinearOrder α] {c : Cardinal.{u}} (hc : 1 < c) (h : IsEta c α) : NoMaxOrder α

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 β) : IsEta c α ↔ IsEta c β

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 β) : IsEta c α = IsEta c β

theorem Order.IsEta.aleph0 {α : Type u} [LinearOrder α] [Nonempty α] [DenselyOrdered α] [NoMaxOrder α] [NoMinOrder α] : IsEta Cardinal.aleph0 α

theorem Order.IsEta.Rat.isEta_aleph0 : IsEta Cardinal.aleph0 ℚ