mathlib documentation

order.locally_finite

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).

Many theorems about these intervals can be found in data.finset.locally_finite.

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,

When it's also an order_top,

When it's also an order_bot,

Instances #

A locally_finite_order instance can be built

Instances for concrete types are proved in their respective files:

TODO #

Provide the locally_finite_order instance for α ×ₗ β 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_max_order α, locally_finite_order α, we can also define an order isomorphism α ≃ ℕ or α ≃ ℤ, depending on whether we have order_bot α or no_min_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.

@[class]
structure locally_finite_order (α : Type u_1) [preorder α] :
Type u_1

A locally finite order is an order where bounded intervals are finite. When you don't care too much about definitional equality, you can use locally_finite_order.of_Icc or locally_finite_order.of_finite_Icc to build a locally finite order from just finset.Icc.

Instances
def locally_finite_order.of_Icc' (α : Type u_1) [preorder α] [decidable_rel has_le.le] (finset_Icc : α → α → finset α) (mem_Icc : ∀ (a b x : α), x finset_Icc a b a x x b) :

A constructor from a definition of finset.Icc alone, the other ones being derived by removing the ends. As opposed to locally_finite_order.of_Icc, this one requires decidable_rel (≤) but only preorder.

Equations
def locally_finite_order.of_Icc (α : Type u_1) [partial_order α] [decidable_eq α] (finset_Icc : α → α → finset α) (mem_Icc : ∀ (a b x : α), x finset_Icc a b a x x b) :

A constructor from a definition of finset.Icc alone, the other ones being derived by removing the ends. As opposed to locally_finite_order.of_Icc, this one requires partial_order but only decidable_eq.

Equations

Intervals as finsets #

def finset.Icc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :

The finset of elements x such that a ≤ x and x ≤ b. Basically set.Icc a b as a finset.

Equations
def finset.Ico {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :

The finset of elements x such that a ≤ x and x < b. Basically set.Ico a b as a finset.

Equations
def finset.Ioc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :

The finset of elements x such that a < x and x ≤ b. Basically set.Ioc a b as a finset.

Equations
def finset.Ioo {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :

The finset of elements x such that a < x and x < b. Basically set.Ioo a b as a finset.

Equations
@[simp]
theorem finset.mem_Icc {α : Type u_1} [preorder α] [locally_finite_order α] {a b x : α} :
x finset.Icc a b a x x b
@[simp]
theorem finset.mem_Ico {α : Type u_1} [preorder α] [locally_finite_order α] {a b x : α} :
x finset.Ico a b a x x < b
@[simp]
theorem finset.mem_Ioc {α : Type u_1} [preorder α] [locally_finite_order α] {a b x : α} :
x finset.Ioc a b a < x x b
@[simp]
theorem finset.mem_Ioo {α : Type u_1} [preorder α] [locally_finite_order α] {a b x : α} :
x finset.Ioo a b a < x x < b
@[simp, norm_cast]
theorem finset.coe_Icc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
@[simp, norm_cast]
theorem finset.coe_Ico {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
@[simp, norm_cast]
theorem finset.coe_Ioc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
@[simp, norm_cast]
theorem finset.coe_Ioo {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
def finset.Ici {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] (a : α) :

The finset of elements x such that a ≤ x. Basically set.Ici a as a finset.

Equations
def finset.Ioi {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] (a : α) :

The finset of elements x such that a < x. Basically set.Ioi a as a finset.

Equations
theorem finset.Ici_eq_Icc {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] (a : α) :
theorem finset.Ioi_eq_Ioc {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] (a : α) :
@[simp, norm_cast]
theorem finset.coe_Ici {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] (a : α) :
@[simp, norm_cast]
theorem finset.coe_Ioi {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] (a : α) :
@[simp]
theorem finset.mem_Ici {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] {a x : α} :
@[simp]
theorem finset.mem_Ioi {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] {a x : α} :
def finset.Iic {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] (b : α) :

The finset of elements x such that x ≤ b. Basically set.Iic b as a finset.

Equations
def finset.Iio {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] (b : α) :

The finset of elements x such that x < b. Basically set.Iio b as a finset.

Equations
@[simp, norm_cast]
theorem finset.coe_Iic {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] (b : α) :
@[simp, norm_cast]
theorem finset.coe_Iio {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] (b : α) :
@[simp]
theorem finset.mem_Iic {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] {b x : α} :
@[simp]
theorem finset.mem_Iio {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] {b x : α} :

Intervals as multisets #

def multiset.Icc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :

The multiset of elements x such that a ≤ x and x ≤ b. Basically set.Icc a b as a multiset.

Equations
def multiset.Ico {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :

The multiset of elements x such that a ≤ x and x < b. Basically set.Ico a b as a multiset.

Equations
def multiset.Ioc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :

The multiset of elements x such that a < x and x ≤ b. Basically set.Ioc a b as a multiset.

Equations
def multiset.Ioo {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :

The multiset of elements x such that a < x and x < b. Basically set.Ioo a b as a multiset.

Equations
@[simp]
theorem multiset.mem_Icc {α : Type u_1} [preorder α] [locally_finite_order α] {a b x : α} :
x multiset.Icc a b a x x b
@[simp]
theorem multiset.mem_Ico {α : Type u_1} [preorder α] [locally_finite_order α] {a b x : α} :
x multiset.Ico a b a x x < b
@[simp]
theorem multiset.mem_Ioc {α : Type u_1} [preorder α] [locally_finite_order α] {a b x : α} :
x multiset.Ioc a b a < x x b
@[simp]
theorem multiset.mem_Ioo {α : Type u_1} [preorder α] [locally_finite_order α] {a b x : α} :
x multiset.Ioo a b a < x x < b
def multiset.Ici {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] (a : α) :

The multiset of elements x such that a ≤ x. Basically set.Ici a as a multiset.

Equations
def multiset.Ioi {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] (a : α) :

The multiset of elements x such that a < x. Basically set.Ioi a as a multiset.

Equations
@[simp]
theorem multiset.mem_Ici {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] {a x : α} :
@[simp]
theorem multiset.mem_Ioi {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] {a x : α} :
def multiset.Iic {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] (b : α) :

The multiset of elements x such that x ≤ b. Basically set.Iic b as a multiset.

Equations
def multiset.Iio {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] (b : α) :

The multiset of elements x such that x < b. Basically set.Iio b as a multiset.

Equations
@[simp]
theorem multiset.mem_Iic {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] {b x : α} :
@[simp]
theorem multiset.mem_Iio {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] {b x : α} :

Finiteness of set intervals #

@[protected, instance]
def set.fintype_Icc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
Equations
@[protected, instance]
def set.fintype_Ico {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
Equations
@[protected, instance]
def set.fintype_Ioc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
Equations
@[protected, instance]
def set.fintype_Ioo {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
Equations
theorem set.finite_Icc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
theorem set.finite_Ico {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
theorem set.finite_Ioc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
theorem set.finite_Ioo {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
@[protected, instance]
def set.fintype_Ici {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] (a : α) :
Equations
@[protected, instance]
def set.fintype_Ioi {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] (a : α) :
Equations
theorem set.finite_Ici {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] (a : α) :
theorem set.finite_Ioi {α : Type u_1} [preorder α] [order_top α] [locally_finite_order α] (a : α) :
@[protected, instance]
def set.fintype_Iic {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] (b : α) :
Equations
@[protected, instance]
def set.fintype_Iio {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] (b : α) :
Equations
theorem set.finite_Iic {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] (b : α) :
theorem set.finite_Iio {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] (b : α) :

Instances #

noncomputable def locally_finite_order.of_finite_Icc {α : Type u_1} [preorder α] (h : ∀ (a b : α), (set.Icc a b).finite) :

A noncomputable constructor from the finiteness of all closed intervals.

Equations
noncomputable def fintype.to_locally_finite_order {α : Type u_1} [preorder α] [fintype α] :

A fintype is noncomputably a locally finite order.

Equations
@[protected, instance]
noncomputable def order_embedding.locally_finite_order {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order β] (f : α ↪o β) :

Given an order embedding α ↪o β, pulls back the locally_finite_order on β to α.

Equations
@[protected, instance]

Note we define Icc (to_dual a) (to_dual b) as Icc α _ _ b a (which has type finset α not finset (order_dual α)!) instead of (Icc b a).map to_dual.to_embedding as this means the following is defeq:

lemma this : (Icc (to_dual (to_dual a)) (to_dual (to_dual b)) : _) = (Icc a b : _) := rfl
Equations
@[protected, instance]
Equations

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.

@[protected, instance]
Equations

Subtype of a locally finite order #

@[protected, instance]
def subtype.locally_finite_order {α : Type u_1} [preorder α] [locally_finite_order α] (p : α → Prop) [decidable_pred p] :
Equations
theorem finset.subtype_Icc_eq {α : Type u_1} [preorder α] [locally_finite_order α] (p : α → Prop) [decidable_pred p] (a b : subtype p) :
theorem finset.subtype_Ico_eq {α : Type u_1} [preorder α] [locally_finite_order α] (p : α → Prop) [decidable_pred p] (a b : subtype p) :
theorem finset.subtype_Ioc_eq {α : Type u_1} [preorder α] [locally_finite_order α] (p : α → Prop) [decidable_pred p] (a b : subtype p) :
theorem finset.subtype_Ioo_eq {α : Type u_1} [preorder α] [locally_finite_order α] (p : α → Prop) [decidable_pred p] (a b : subtype p) :
theorem finset.map_subtype_embedding_Icc {α : Type u_1} [preorder α] [locally_finite_order α] (p : α → Prop) [decidable_pred p] (a b : subtype p) (hp : ∀ ⦃a b x : α⦄, a xx bp ap bp x) :
theorem finset.map_subtype_embedding_Ico {α : Type u_1} [preorder α] [locally_finite_order α] (p : α → Prop) [decidable_pred p] (a b : subtype p) (hp : ∀ ⦃a b x : α⦄, a xx bp ap bp x) :
theorem finset.map_subtype_embedding_Ioc {α : Type u_1} [preorder α] [locally_finite_order α] (p : α → Prop) [decidable_pred p] (a b : subtype p) (hp : ∀ ⦃a b x : α⦄, a xx bp ap bp x) :
theorem finset.map_subtype_embedding_Ioo {α : Type u_1} [preorder α] [locally_finite_order α] (p : α → Prop) [decidable_pred p] (a b : subtype p) (hp : ∀ ⦃a b x : α⦄, a xx bp ap bp x) :