mathlib3 documentation

order.locally_finite

Locally finite orders #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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,

In a locally_finite_order_top,

In a locally_finite_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 of this typeclass
Instances of other typeclasses for locally_finite_order
@[class]
structure locally_finite_order_top (α : Type u_1) [preorder α] :
Type u_1

A locally finite order top is an order where all intervals bounded above are finite. This is slightly weaker than locally_finite_order + order_top as it allows empty types.

Instances of this typeclass
Instances of other typeclasses for locally_finite_order_top
@[class]
structure locally_finite_order_bot (α : Type u_1) [preorder α] :
Type u_1

A locally finite order bot is an order where all intervals bounded below are finite. This is slightly weaker than locally_finite_order + order_bot as it allows empty types.

Instances of this typeclass
Instances of other typeclasses for locally_finite_order_bot
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
def locally_finite_order_top.of_Ici' (α : Type u_1) [preorder α] [decidable_rel has_le.le] (finset_Ici : α finset α) (mem_Ici : (a x : α), x finset_Ici a a x) :

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

Equations
def locally_finite_order_top.of_Ici (α : Type u_1) [partial_order α] [decidable_eq α] (finset_Ici : α finset α) (mem_Ici : (a x : α), x finset_Ici a a x) :

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

Equations
def locally_finite_order_bot.of_Iic' (α : Type u_1) [preorder α] [decidable_rel has_le.le] (finset_Iic : α finset α) (mem_Iic : (a x : α), x finset_Iic a x a) :

A constructor from a definition of finset.Iic 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_top.of_Iic (α : Type u_1) [partial_order α] [decidable_eq α] (finset_Iic : α finset α) (mem_Iic : (a x : α), x finset_Iic a x a) :

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

Equations
@[protected, reducible]

An empty type is locally finite.

This is not an instance as it would not be defeq to more specific instances.

Equations
@[protected, reducible]

An empty type is locally finite.

This is not an instance as it would not be defeq to more specific instances.

Equations
@[protected, reducible]

An empty type is locally finite.

This is not an instance as it would not be defeq to more specific instances.

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 α] [locally_finite_order_top α] (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 α] [locally_finite_order_top α] (a : α) :

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

Equations
@[simp]
theorem finset.mem_Ici {α : Type u_1} [preorder α] [locally_finite_order_top α] {a x : α} :
@[simp]
theorem finset.mem_Ioi {α : Type u_1} [preorder α] [locally_finite_order_top α] {a x : α} :
@[simp, norm_cast]
theorem finset.coe_Ici {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : α) :
@[simp, norm_cast]
theorem finset.coe_Ioi {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : α) :
def finset.Iic {α : Type u_1} [preorder α] [locally_finite_order_bot α] (a : α) :

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

Equations
def finset.Iio {α : Type u_1} [preorder α] [locally_finite_order_bot α] (a : α) :

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

Equations
@[simp]
theorem finset.mem_Iic {α : Type u_1} [preorder α] [locally_finite_order_bot α] {a x : α} :
@[simp]
theorem finset.mem_Iio {α : Type u_1} [preorder α] [locally_finite_order_bot α] {a x : α} :
@[simp, norm_cast]
theorem finset.coe_Iic {α : Type u_1} [preorder α] [locally_finite_order_bot α] (a : α) :
@[simp, norm_cast]
theorem finset.coe_Iio {α : Type u_1} [preorder α] [locally_finite_order_bot α] (a : α) :
theorem finset.Ici_eq_Icc {α : Type u_1} [preorder α] [locally_finite_order α] [order_top α] (a : α) :
theorem finset.Ioi_eq_Ioc {α : Type u_1} [preorder α] [locally_finite_order α] [order_top α] (a : α) :
def finset.uIcc {α : Type u_1} [lattice α] [locally_finite_order α] (a b : α) :

finset.uIcc a b is the set of elements lying between a and b, with a and b included. Note that we define it more generally in a lattice as finset.Icc (a ⊓ b) (a ⊔ b). In a product type, finset.uIcc corresponds to the bounding box of the two elements.

Equations
@[simp]
theorem finset.mem_uIcc {α : Type u_1} [lattice α] [locally_finite_order α] {a b x : α} :
x finset.uIcc a b a b x x a b
@[simp, norm_cast]
theorem finset.coe_uIcc {α : Type u_1} [lattice α] [locally_finite_order α] (a b : α) :

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 α] [locally_finite_order_top α] (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 α] [locally_finite_order_top α] (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 α] [locally_finite_order_top α] {a x : α} :
@[simp]
theorem multiset.mem_Ioi {α : Type u_1} [preorder α] [locally_finite_order_top α] {a x : α} :
def multiset.Iic {α : Type u_1} [preorder α] [locally_finite_order_bot α] (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 α] [locally_finite_order_bot α] (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 α] [locally_finite_order_bot α] {b x : α} :
@[simp]
theorem multiset.mem_Iio {α : Type u_1} [preorder α] [locally_finite_order_bot α] {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 α] [locally_finite_order_top α] (a : α) :
Equations
@[protected, instance]
def set.fintype_Ioi {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : α) :
Equations
theorem set.finite_Ici {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : α) :
theorem set.finite_Ioi {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : α) :
@[protected, instance]
def set.fintype_Iic {α : Type u_1} [preorder α] [locally_finite_order_bot α] (b : α) :
Equations
@[protected, instance]
def set.fintype_Iio {α : Type u_1} [preorder α] [locally_finite_order_bot α] (b : α) :
Equations
theorem set.finite_Iic {α : Type u_1} [preorder α] [locally_finite_order_bot α] (b : α) :
theorem set.finite_Iio {α : Type u_1} [preorder α] [locally_finite_order_bot α] (b : α) :
@[protected, instance]
def set.fintype_uIcc {α : Type u_1} [lattice α] [locally_finite_order α] (a b : α) :
Equations
@[simp]
theorem set.finite_interval {α : Type u_1} [lattice α] [locally_finite_order α] (a 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
@[reducible]

A fintype is a locally finite order.

This is not an instance as it would not be defeq to better instances such as fin.locally_finite_order.

Equations
@[protected, instance]
@[protected]
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 αᵒᵈ!) 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]

Note we define Iic (to_dual a) as Ici a (which has type finset α not finset αᵒᵈ!) instead of (Ici a).map to_dual.to_embedding as this means the following is defeq:

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

Note we define Ici (to_dual a) as Iic a (which has type finset α not finset αᵒᵈ!) instead of (Iic a).map to_dual.to_embedding as this means the following is defeq:

lemma this : (Ici (to_dual (to_dual a)) : _) = (Ici a : _) := rfl
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem prod.Icc_eq {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] [decidable_rel has_le.le] (p q : α × β) :
@[simp]
theorem prod.Icc_mk_mk {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] [decidable_rel has_le.le] (a₁ a₂ : α) (b₁ b₂ : β) :
finset.Icc (a₁, b₁) (a₂, b₂) = finset.Icc a₁ a₂ ×ˢ finset.Icc b₁ b₂
theorem prod.card_Icc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] [decidable_rel has_le.le] (p q : α × β) :
@[simp]
theorem prod.uIcc_mk_mk {α : Type u_1} {β : Type u_2} [lattice α] [lattice β] [locally_finite_order α] [locally_finite_order β] [decidable_rel has_le.le] (a₁ a₂ : α) (b₁ b₂ : β) :
finset.uIcc (a₁, b₁) (a₂, b₂) = finset.uIcc a₁ a₂ ×ˢ finset.uIcc b₁ b₂
theorem prod.card_uIcc {α : Type u_1} {β : Type u_2} [lattice α] [lattice β] [locally_finite_order α] [locally_finite_order β] [decidable_rel has_le.le] (p q : α × β) :

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

Transfer locally finite orders across order isomorphisms #

@[reducible]
def order_iso.locally_finite_order {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order β] (f : α ≃o β) :

Transfer locally_finite_order across an order_iso.

Equations

Subtype of a locally finite order #

theorem finset.subtype_Icc_eq {α : Type u_1} [preorder α] (p : α Prop) [decidable_pred p] [locally_finite_order α] (a b : subtype p) :
theorem finset.subtype_Ico_eq {α : Type u_1} [preorder α] (p : α Prop) [decidable_pred p] [locally_finite_order α] (a b : subtype p) :
theorem finset.subtype_Ioc_eq {α : Type u_1} [preorder α] (p : α Prop) [decidable_pred p] [locally_finite_order α] (a b : subtype p) :
theorem finset.subtype_Ioo_eq {α : Type u_1} [preorder α] (p : α Prop) [decidable_pred p] [locally_finite_order α] (a b : subtype p) :
theorem finset.map_subtype_embedding_Icc {α : Type u_1} [preorder α] (p : α Prop) [decidable_pred p] [locally_finite_order α] (a b : subtype p) (hp : ⦃a b x : α⦄, a x x b p a p b p x) :
theorem finset.map_subtype_embedding_Ico {α : Type u_1} [preorder α] (p : α Prop) [decidable_pred p] [locally_finite_order α] (a b : subtype p) (hp : ⦃a b x : α⦄, a x x b p a p b p x) :
theorem finset.map_subtype_embedding_Ioc {α : Type u_1} [preorder α] (p : α Prop) [decidable_pred p] [locally_finite_order α] (a b : subtype p) (hp : ⦃a b x : α⦄, a x x b p a p b p x) :
theorem finset.map_subtype_embedding_Ioo {α : Type u_1} [preorder α] (p : α Prop) [decidable_pred p] [locally_finite_order α] (a b : subtype p) (hp : ⦃a b x : α⦄, a x x b p a p b p x) :
theorem finset.map_subtype_embedding_Ici {α : Type u_1} [preorder α] (p : α Prop) [decidable_pred p] [locally_finite_order_top α] (a : subtype p) (hp : ⦃a x : α⦄, a x p a p x) :
theorem finset.map_subtype_embedding_Ioi {α : Type u_1} [preorder α] (p : α Prop) [decidable_pred p] [locally_finite_order_top α] (a : subtype p) (hp : ⦃a x : α⦄, a x p a p x) :
theorem finset.map_subtype_embedding_Iic {α : Type u_1} [preorder α] (p : α Prop) [decidable_pred p] [locally_finite_order_bot α] (a : subtype p) (hp : ⦃a x : α⦄, x a p a p x) :
theorem finset.map_subtype_embedding_Iio {α : Type u_1} [preorder α] (p : α Prop) [decidable_pred p] [locally_finite_order_bot α] (a : subtype p) (hp : ⦃a x : α⦄, x a p a p x) :