Locally finite orders #

This file defines locally finite orders.

A locally finite order is an order for which all bounded intervals are finite. This allows to make sense of Icc/Ico/Ioc/Ioo as lists, multisets, or finsets. Further, if the order is bounded above (resp. below), then we can also make sense of the "unbounded" intervals Ici/Ioi (resp. Iic/Iio).

Examples #

Naturally occurring locally finite orders are ℕ, ℤ, ℕ+, fin n, α × β the product of two locally finite orders, α →₀ β the finitely supported functions to a locally finite order β...

Main declarations #

In a locally_finite_order,

• finset.Icc: Closed-closed interval as a finset.
• finset.Ico: Closed-open interval as a finset.
• finset.Ioc: Open-closed interval as a finset.
• finset.Ioo: Open-open interval as a finset.
• multiset.Icc: Closed-closed interval as a multiset.
• multiset.Ico: Closed-open interval as a multiset.
• multiset.Ioc: Open-closed interval as a multiset.
• multiset.Ioo: Open-open interval as a multiset.

When it's also an order_top,

• finset.Ici: Closed-infinite interval as a finset.
• finset.Ioi: Open-infinite interval as a finset.
• multiset.Ici: Closed-infinite interval as a multiset.
• multiset.Ioi: Open-infinite interval as a multiset.

When it's also an order_bot,

• finset.Iic: Infinite-open interval as a finset.
• finset.Iio: Infinite-closed interval as a finset.
• multiset.Iic: Infinite-open interval as a multiset.
• multiset.Iio: Infinite-closed interval as a multiset.

Instances #

A locally_finite_order instance can be built

• for a subtype of a locally finite order. See subtype.locally_finite_order.
• for the product of two locally finite orders. See prod.locally_finite_order.
• for any fintype (but it is noncomputable). See fintype.to_locally_finite_order.
• from a definition of finset.Icc alone. See locally_finite_order.of_Icc.
• by pulling back locally_finite_order β through an order embedding f : α →o β. See order_embedding.locally_finite_order.

Instances for concrete types are proved in their respective files:

• ℕ is in data.nat.interval
• ℤ is in data.int.interval
• ℕ+ is in data.pnat.interval
• fin n is in data.fin.interval
• finset α is in data.finset.interval Along, you will find lemmas about the cardinality of those finite intervals.

TODO #

Provide the locally_finite_order instance for lex α β where locally_finite_order α and fintype β.

Provide the locally_finite_order instance for α →₀ β where β is locally finite. Provide the locally_finite_order instance for Π₀ i, β i where all the β i are locally finite.

From linear_order α, no_top_order α, locally_finite_order α, we can also define an order isomorphism α ≃ ℕ or α ≃ ℤ, depending on whether we have order_bot α or no_bot_order α and nonempty α. When order_bot α, we can match a : α to (Iio a).card.

We can provide succ_order α from linear_order α and locally_finite_order α using

lemma exists_min_greater [linear_order α] [locally_finite_order α] {x ub : α} (hx : x < ub) :
  ∃ lub, x < lub ∧ ∀ y, x < y → lub ≤ y :=
begin -- very non golfed
  have h : (finset.Ioc x ub).nonempty := ⟨ub, finset.mem_Ioc_iff.2 ⟨hx, le_rfl⟩⟩,
  use finset.min' (finset.Ioc x ub) h,
  split,
  { have := finset.min'_mem _ h,
    simp * at * },
  rintro y hxy,
  obtain hy | hy := le_total y ub,
  apply finset.min'_le,
  simp * at *,
  exact (finset.min'_le _ _ (finset.mem_Ioc_iff.2 ⟨hx, le_rfl⟩)).trans hy,
end

Note that the converse is not true. Consider {-2^z | z : ℤ} ∪ {2^z | z : ℤ}. Any element has a successor (and actually a predecessor as well), so it is a succ_order, but it's not locally finite as Icc (-1) 1 is infinite.

Intervals as finsets #

Intervals as multisets #

Finiteness of set intervals #

Instances #

with_top, with_bot #

Adding a ⊤ to a locally finite order_top keeps it locally finite. Adding a ⊥ to a locally finite order_bot keeps it locally finite.

Subtype of a locally finite order #