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.

source
@[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
source
@[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
source
@[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
source
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) :
locally_finite_order α

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
source
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) :
locally_finite_order α

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
source
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) :
locally_finite_order_top α

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
source
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) :
locally_finite_order_top α

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
source
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) :
locally_finite_order_bot α

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
source
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) :
locally_finite_order_bot α

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
source
@[protected, reducible]
def is_empty.to_locally_finite_order {α : Type u_1} [preorder α] [is_empty α] :
locally_finite_order α

An empty type is locally finite.

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

Equations
source
@[protected, reducible]
def is_empty.to_locally_finite_order_top {α : Type u_1} [preorder α] [is_empty α] :
locally_finite_order_top α

An empty type is locally finite.

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

Equations
source
@[protected, reducible]
def is_empty.to_locally_finite_order_bot {α : Type u_1} [preorder α] [is_empty α] :
locally_finite_order_bot α

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 #

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

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

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

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

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

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

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

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

Equations
source
@[simp]
theorem finset.mem_Icc {α : Type u_1} [preorder α] [locally_finite_order α] {a b x : α} :
x ∈ finset.Icc a b ↔ a ≤ x ∧ x ≤ b
source
@[simp]
theorem finset.mem_Ico {α : Type u_1} [preorder α] [locally_finite_order α] {a b x : α} :
x ∈ finset.Ico a b ↔ a ≤ x ∧ x < b
source
@[simp]
theorem finset.mem_Ioc {α : Type u_1} [preorder α] [locally_finite_order α] {a b x : α} :
x ∈ finset.Ioc a b ↔ a < x ∧ x ≤ b
source
@[simp]
theorem finset.mem_Ioo {α : Type u_1} [preorder α] [locally_finite_order α] {a b x : α} :
x ∈ finset.Ioo a b ↔ a < x ∧ x < b
source
@[simp, norm_cast]
theorem finset.coe_Icc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
↑(finset.Icc a b) = set.Icc a b
source
@[simp, norm_cast]
theorem finset.coe_Ico {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
↑(finset.Ico a b) = set.Ico a b
source
@[simp, norm_cast]
theorem finset.coe_Ioc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
↑(finset.Ioc a b) = set.Ioc a b
source
@[simp, norm_cast]
theorem finset.coe_Ioo {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
↑(finset.Ioo a b) = set.Ioo a b
source
def finset.Ici {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : α) :
finset α

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

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

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

Equations
source
@[simp]
theorem finset.mem_Ici {α : Type u_1} [preorder α] [locally_finite_order_top α] {a x : α} :
x ∈ finset.Ici a ↔ a ≤ x
source
@[simp]
theorem finset.mem_Ioi {α : Type u_1} [preorder α] [locally_finite_order_top α] {a x : α} :
x ∈ finset.Ioi a ↔ a < x
source
@[simp, norm_cast]
theorem finset.coe_Ici {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : α) :
↑(finset.Ici a) = set.Ici a
source
@[simp, norm_cast]
theorem finset.coe_Ioi {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : α) :
↑(finset.Ioi a) = set.Ioi a
source
def finset.Iic {α : Type u_1} [preorder α] [locally_finite_order_bot α] (a : α) :
finset α

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

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

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

Equations
source
@[simp]
theorem finset.mem_Iic {α : Type u_1} [preorder α] [locally_finite_order_bot α] {a x : α} :
x ∈ finset.Iic a ↔ x ≤ a
source
@[simp]
theorem finset.mem_Iio {α : Type u_1} [preorder α] [locally_finite_order_bot α] {a x : α} :
x ∈ finset.Iio a ↔ x < a
source
@[simp, norm_cast]
theorem finset.coe_Iic {α : Type u_1} [preorder α] [locally_finite_order_bot α] (a : α) :
↑(finset.Iic a) = set.Iic a
source
@[simp, norm_cast]
theorem finset.coe_Iio {α : Type u_1} [preorder α] [locally_finite_order_bot α] (a : α) :
↑(finset.Iio a) = set.Iio a
source
@[protected, instance]
def locally_finite_order.to_locally_finite_order_top {α : Type u_1} [preorder α] [locally_finite_order α] [order_top α] :
locally_finite_order_top α
Equations
source
theorem finset.Ici_eq_Icc {α : Type u_1} [preorder α] [locally_finite_order α] [order_top α] (a : α) :
finset.Ici a = finset.Icc a ⊤
source
theorem finset.Ioi_eq_Ioc {α : Type u_1} [preorder α] [locally_finite_order α] [order_top α] (a : α) :
finset.Ioi a = finset.Ioc a ⊤
source
@[protected, instance]
def finset.locally_finite_order.to_locally_finite_order_bot {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] :
locally_finite_order_bot α
Equations
source
theorem finset.Iic_eq_Icc {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] :
finset.Iic = finset.Icc ⊥
source
theorem finset.Iio_eq_Ico {α : Type u_1} [preorder α] [order_bot α] [locally_finite_order α] :
finset.Iio = finset.Ico ⊥
source
def finset.uIcc {α : Type u_1} [lattice α] [locally_finite_order α] (a b : α) :
finset α

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
source
@[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
source
@[simp, norm_cast]
theorem finset.coe_uIcc {α : Type u_1} [lattice α] [locally_finite_order α] (a b : α) :
↑(finset.uIcc a b) = set.uIcc a b

Intervals as multisets #

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

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

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

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

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

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

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

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

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

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

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

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

Equations
source
@[simp]
theorem multiset.mem_Ici {α : Type u_1} [preorder α] [locally_finite_order_top α] {a x : α} :
x ∈ multiset.Ici a ↔ a ≤ x
source
@[simp]
theorem multiset.mem_Ioi {α : Type u_1} [preorder α] [locally_finite_order_top α] {a x : α} :
x ∈ multiset.Ioi a ↔ a < x
source
def multiset.Iic {α : Type u_1} [preorder α] [locally_finite_order_bot α] (b : α) :
multiset α

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

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

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

Equations
source
@[simp]
theorem multiset.mem_Iic {α : Type u_1} [preorder α] [locally_finite_order_bot α] {b x : α} :
x ∈ multiset.Iic b ↔ x ≤ b
source
@[simp]
theorem multiset.mem_Iio {α : Type u_1} [preorder α] [locally_finite_order_bot α] {b x : α} :
x ∈ multiset.Iio b ↔ x < b

Finiteness of set intervals #

source
@[protected, instance]
def set.fintype_Icc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
fintype ↥(set.Icc a b)
Equations
source
@[protected, instance]
def set.fintype_Ico {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
fintype ↥(set.Ico a b)
Equations
source
@[protected, instance]
def set.fintype_Ioc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
fintype ↥(set.Ioc a b)
Equations
source
@[protected, instance]
def set.fintype_Ioo {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
fintype ↥(set.Ioo a b)
Equations
source
theorem set.finite_Icc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
(set.Icc a b).finite
source
theorem set.finite_Ico {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
(set.Ico a b).finite
source
theorem set.finite_Ioc {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
(set.Ioc a b).finite
source
theorem set.finite_Ioo {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
(set.Ioo a b).finite
source
@[protected, instance]
def set.fintype_Ici {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : α) :
fintype ↥(set.Ici a)
Equations
source
@[protected, instance]
def set.fintype_Ioi {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : α) :
fintype ↥(set.Ioi a)
Equations
source
theorem set.finite_Ici {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : α) :
(set.Ici a).finite
source
theorem set.finite_Ioi {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : α) :
(set.Ioi a).finite
source
@[protected, instance]
def set.fintype_Iic {α : Type u_1} [preorder α] [locally_finite_order_bot α] (b : α) :
fintype ↥(set.Iic b)
Equations
source
@[protected, instance]
def set.fintype_Iio {α : Type u_1} [preorder α] [locally_finite_order_bot α] (b : α) :
fintype ↥(set.Iio b)
Equations
source
theorem set.finite_Iic {α : Type u_1} [preorder α] [locally_finite_order_bot α] (b : α) :
(set.Iic b).finite
source
theorem set.finite_Iio {α : Type u_1} [preorder α] [locally_finite_order_bot α] (b : α) :
(set.Iio b).finite
source
@[protected, instance]
def set.fintype_uIcc {α : Type u_1} [lattice α] [locally_finite_order α] (a b : α) :
fintype ↥(set.uIcc a b)
Equations
source
@[simp]
theorem set.finite_interval {α : Type u_1} [lattice α] [locally_finite_order α] (a b : α) :
(set.uIcc a b).finite

Instances #

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

A noncomputable constructor from the finiteness of all closed intervals.

Equations
source
@[reducible]
def fintype.to_locally_finite_order {α : Type u_1} [preorder α] [fintype α] [decidable_rel has_lt.lt] [decidable_rel has_le.le] :
locally_finite_order α

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
source
@[protected, instance]
def locally_finite_order.subsingleton {α : Type u_1} [preorder α] :
subsingleton (locally_finite_order α)
source
@[protected, instance]
def locally_finite_order_top.subsingleton {α : Type u_1} [preorder α] :
subsingleton (locally_finite_order_top α)
source
@[protected, instance]
def locally_finite_order_bot.subsingleton {α : Type u_1} [preorder α] :
subsingleton (locally_finite_order_bot α)
source
@[protected]
noncomputable def order_embedding.locally_finite_order {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order β] (f : α ↪o β) :
locally_finite_order α

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

Equations
source
@[protected, instance]
def order_dual.locally_finite_order {α : Type u_1} [preorder α] [locally_finite_order α] :
locally_finite_order αᵒᵈ

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
source
theorem Icc_to_dual {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
finset.Icc (⇑order_dual.to_dual a) (⇑order_dual.to_dual b) = finset.map order_dual.to_dual.to_embedding (finset.Icc b a)
source
theorem Ico_to_dual {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
finset.Ico (⇑order_dual.to_dual a) (⇑order_dual.to_dual b) = finset.map order_dual.to_dual.to_embedding (finset.Ioc b a)
source
theorem Ioc_to_dual {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
finset.Ioc (⇑order_dual.to_dual a) (⇑order_dual.to_dual b) = finset.map order_dual.to_dual.to_embedding (finset.Ico b a)
source
theorem Ioo_to_dual {α : Type u_1} [preorder α] [locally_finite_order α] (a b : α) :
finset.Ioo (⇑order_dual.to_dual a) (⇑order_dual.to_dual b) = finset.map order_dual.to_dual.to_embedding (finset.Ioo b a)
source
theorem Icc_of_dual {α : Type u_1} [preorder α] [locally_finite_order α] (a b : αᵒᵈ) :
finset.Icc (⇑order_dual.of_dual a) (⇑order_dual.of_dual b) = finset.map order_dual.of_dual.to_embedding (finset.Icc b a)
source
theorem Ico_of_dual {α : Type u_1} [preorder α] [locally_finite_order α] (a b : αᵒᵈ) :
finset.Ico (⇑order_dual.of_dual a) (⇑order_dual.of_dual b) = finset.map order_dual.of_dual.to_embedding (finset.Ioc b a)
source
theorem Ioc_of_dual {α : Type u_1} [preorder α] [locally_finite_order α] (a b : αᵒᵈ) :
finset.Ioc (⇑order_dual.of_dual a) (⇑order_dual.of_dual b) = finset.map order_dual.of_dual.to_embedding (finset.Ico b a)
source
theorem Ioo_of_dual {α : Type u_1} [preorder α] [locally_finite_order α] (a b : αᵒᵈ) :
finset.Ioo (⇑order_dual.of_dual a) (⇑order_dual.of_dual b) = finset.map order_dual.of_dual.to_embedding (finset.Ioo b a)
source
@[protected, instance]
def order_dual.locally_finite_order_bot {α : Type u_1} [preorder α] [locally_finite_order_top α] :
locally_finite_order_bot αᵒᵈ

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
source
theorem Iic_to_dual {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : α) :
finset.Iic (⇑order_dual.to_dual a) = finset.map order_dual.to_dual.to_embedding (finset.Ici a)
source
theorem Iio_to_dual {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : α) :
finset.Iio (⇑order_dual.to_dual a) = finset.map order_dual.to_dual.to_embedding (finset.Ioi a)
source
theorem Ici_of_dual {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : αᵒᵈ) :
finset.Ici (⇑order_dual.of_dual a) = finset.map order_dual.of_dual.to_embedding (finset.Iic a)
source
theorem Ioi_of_dual {α : Type u_1} [preorder α] [locally_finite_order_top α] (a : αᵒᵈ) :
finset.Ioi (⇑order_dual.of_dual a) = finset.map order_dual.of_dual.to_embedding (finset.Iio a)
source
@[protected, instance]
def order_dual.locally_finite_order_top {α : Type u_1} [preorder α] [locally_finite_order_bot α] :
locally_finite_order_top αᵒᵈ

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
source
theorem Ici_to_dual {α : Type u_1} [preorder α] [locally_finite_order_bot α] (a : α) :
finset.Ici (⇑order_dual.to_dual a) = finset.map order_dual.to_dual.to_embedding (finset.Iic a)
source
theorem Ioi_to_dual {α : Type u_1} [preorder α] [locally_finite_order_bot α] (a : α) :
finset.Ioi (⇑order_dual.to_dual a) = finset.map order_dual.to_dual.to_embedding (finset.Iio a)
source
theorem Iic_of_dual {α : Type u_1} [preorder α] [locally_finite_order_bot α] (a : αᵒᵈ) :
finset.Iic (⇑order_dual.of_dual a) = finset.map order_dual.of_dual.to_embedding (finset.Ici a)
source
theorem Iio_of_dual {α : Type u_1} [preorder α] [locally_finite_order_bot α] (a : αᵒᵈ) :
finset.Iio (⇑order_dual.of_dual a) = finset.map order_dual.of_dual.to_embedding (finset.Ioi a)
source
@[protected, instance]
def prod.locally_finite_order {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order α] [locally_finite_order β] [decidable_rel has_le.le] :
locally_finite_order (α × β)
Equations
source
@[protected, instance]
def prod.locally_finite_order_top {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order_top α] [locally_finite_order_top β] [decidable_rel has_le.le] :
locally_finite_order_top (α × β)
Equations
source
@[protected, instance]
def prod.locally_finite_order_bot {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [locally_finite_order_bot α] [locally_finite_order_bot β] [decidable_rel has_le.le] :
locally_finite_order_bot (α × β)
Equations
source
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 : α × β) :
finset.Icc p q = finset.Icc p.fst q.fst ×ˢ finset.Icc p.snd q.snd
source
@[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₂
source
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 : α × β) :
(finset.Icc p q).card = (finset.Icc p.fst q.fst).card * (finset.Icc p.snd q.snd).card
source
theorem prod.uIcc_eq {α : Type u_1} {β : Type u_2} [lattice α] [lattice β] [locally_finite_order α] [locally_finite_order β] [decidable_rel has_le.le] (p q : α × β) :
finset.uIcc p q = finset.uIcc p.fst q.fst ×ˢ finset.uIcc p.snd q.snd
source
@[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₂
source
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 : α × β) :
(finset.uIcc p q).card = (finset.uIcc p.fst q.fst).card * (finset.uIcc p.snd q.snd).card

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.

source
@[protected, instance]
def with_top.locally_finite_order (α : Type u_1) [partial_order α] [order_top α] [locally_finite_order α] :
locally_finite_order (with_top α)
Equations
source
theorem with_top.Icc_coe_top (α : Type u_1) [partial_order α] [order_top α] [locally_finite_order α] (a : α) :
finset.Icc ↑a ⊤ = ⇑finset.insert_none (finset.Ici a)
source
theorem with_top.Icc_coe_coe (α : Type u_1) [partial_order α] [order_top α] [locally_finite_order α] (a b : α) :
finset.Icc ↑a ↑b = finset.map function.embedding.coe_option (finset.Icc a b)
source
theorem with_top.Ico_coe_top (α : Type u_1) [partial_order α] [order_top α] [locally_finite_order α] (a : α) :
finset.Ico ↑a ⊤ = finset.map function.embedding.coe_option (finset.Ici a)
source
theorem with_top.Ico_coe_coe (α : Type u_1) [partial_order α] [order_top α] [locally_finite_order α] (a b : α) :
finset.Ico ↑a ↑b = finset.map function.embedding.coe_option (finset.Ico a b)
source
theorem with_top.Ioc_coe_top (α : Type u_1) [partial_order α] [order_top α] [locally_finite_order α] (a : α) :
finset.Ioc ↑a ⊤ = ⇑finset.insert_none (finset.Ioi a)
source
theorem with_top.Ioc_coe_coe (α : Type u_1) [partial_order α] [order_top α] [locally_finite_order α] (a b : α) :
finset.Ioc ↑a ↑b = finset.map function.embedding.coe_option (finset.Ioc a b)
source
theorem with_top.Ioo_coe_top (α : Type u_1) [partial_order α] [order_top α] [locally_finite_order α] (a : α) :
finset.Ioo ↑a ⊤ = finset.map function.embedding.coe_option (finset.Ioi a)
source
theorem with_top.Ioo_coe_coe (α : Type u_1) [partial_order α] [order_top α] [locally_finite_order α] (a b : α) :
finset.Ioo ↑a ↑b = finset.map function.embedding.coe_option (finset.Ioo a b)
source
@[protected, instance]
def with_bot.locally_finite_order (α : Type u_1) [partial_order α] [order_bot α] [locally_finite_order α] :
locally_finite_order (with_bot α)
Equations
source
theorem with_bot.Icc_bot_coe (α : Type u_1) [partial_order α] [order_bot α] [locally_finite_order α] (b : α) :
finset.Icc ⊥ ↑b = ⇑finset.insert_none (finset.Iic b)
source
theorem with_bot.Icc_coe_coe (α : Type u_1) [partial_order α] [order_bot α] [locally_finite_order α] (a b : α) :
finset.Icc ↑a ↑b = finset.map function.embedding.coe_option (finset.Icc a b)
source
theorem with_bot.Ico_bot_coe (α : Type u_1) [partial_order α] [order_bot α] [locally_finite_order α] (b : α) :
finset.Ico ⊥ ↑b = ⇑finset.insert_none (finset.Iio b)
source
theorem with_bot.Ico_coe_coe (α : Type u_1) [partial_order α] [order_bot α] [locally_finite_order α] (a b : α) :
finset.Ico ↑a ↑b = finset.map function.embedding.coe_option (finset.Ico a b)
source
theorem with_bot.Ioc_bot_coe (α : Type u_1) [partial_order α] [order_bot α] [locally_finite_order α] (b : α) :
finset.Ioc ⊥ ↑b = finset.map function.embedding.coe_option (finset.Iic b)
source
theorem with_bot.Ioc_coe_coe (α : Type u_1) [partial_order α] [order_bot α] [locally_finite_order α] (a b : α) :
finset.Ioc ↑a ↑b = finset.map function.embedding.coe_option (finset.Ioc a b)
source
theorem with_bot.Ioo_bot_coe (α : Type u_1) [partial_order α] [order_bot α] [locally_finite_order α] (b : α) :
finset.Ioo ⊥ ↑b = finset.map function.embedding.coe_option (finset.Iio b)
source
theorem with_bot.Ioo_coe_coe (α : Type u_1) [partial_order α] [order_bot α] [locally_finite_order α] (a b : α) :
finset.Ioo ↑a ↑b = finset.map function.embedding.coe_option (finset.Ioo a b)

Transfer locally finite orders across order isomorphisms #

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

Transfer locally_finite_order across an order_iso.

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

Transfer locally_finite_order_top across an order_iso.

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

Transfer locally_finite_order_bot across an order_iso.

Equations

Subtype of a locally finite order #

source
@[protected, instance]
def subtype.locally_finite_order {α : Type u_1} [preorder α] (p : α → Prop) [decidable_pred p] [locally_finite_order α] :
locally_finite_order (subtype p)
Equations
source
@[protected, instance]
def subtype.locally_finite_order_top {α : Type u_1} [preorder α] (p : α → Prop) [decidable_pred p] [locally_finite_order_top α] :
locally_finite_order_top (subtype p)
Equations
source
@[protected, instance]
def subtype.locally_finite_order_bot {α : Type u_1} [preorder α] (p : α → Prop) [decidable_pred p] [locally_finite_order_bot α] :
locally_finite_order_bot (subtype p)
Equations
source
theorem finset.subtype_Icc_eq {α : Type u_1} [preorder α] (p : α → Prop) [decidable_pred p] [locally_finite_order α] (a b : subtype p) :
finset.Icc a b = finset.subtype p (finset.Icc ↑a ↑b)
source
theorem finset.subtype_Ico_eq {α : Type u_1} [preorder α] (p : α → Prop) [decidable_pred p] [locally_finite_order α] (a b : subtype p) :
finset.Ico a b = finset.subtype p (finset.Ico ↑a ↑b)
source
theorem finset.subtype_Ioc_eq {α : Type u_1} [preorder α] (p : α → Prop) [decidable_pred p] [locally_finite_order α] (a b : subtype p) :
finset.Ioc a b = finset.subtype p (finset.Ioc ↑a ↑b)
source
theorem finset.subtype_Ioo_eq {α : Type u_1} [preorder α] (p : α → Prop) [decidable_pred p] [locally_finite_order α] (a b : subtype p) :
finset.Ioo a b = finset.subtype p (finset.Ioo ↑a ↑b)
source
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) :
finset.map (function.embedding.subtype p) (finset.Icc a b) = finset.Icc ↑a ↑b
source
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) :
finset.map (function.embedding.subtype p) (finset.Ico a b) = finset.Ico ↑a ↑b
source
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) :
finset.map (function.embedding.subtype p) (finset.Ioc a b) = finset.Ioc ↑a ↑b
source
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) :
finset.map (function.embedding.subtype p) (finset.Ioo a b) = finset.Ioo ↑a ↑b
source
theorem finset.subtype_Ici_eq {α : Type u_1} [preorder α] (p : α → Prop) [decidable_pred p] [locally_finite_order_top α] (a : subtype p) :
finset.Ici a = finset.subtype p (finset.Ici ↑a)
source
theorem finset.subtype_Ioi_eq {α : Type u_1} [preorder α] (p : α → Prop) [decidable_pred p] [locally_finite_order_top α] (a : subtype p) :
finset.Ioi a = finset.subtype p (finset.Ioi ↑a)
source
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) :
finset.map (function.embedding.subtype p) (finset.Ici a) = finset.Ici ↑a
source
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) :
finset.map (function.embedding.subtype p) (finset.Ioi a) = finset.Ioi ↑a
source
theorem finset.subtype_Iic_eq {α : Type u_1} [preorder α] (p : α → Prop) [decidable_pred p] [locally_finite_order_bot α] (a : subtype p) :
finset.Iic a = finset.subtype p (finset.Iic ↑a)
source
theorem finset.subtype_Iio_eq {α : Type u_1} [preorder α] (p : α → Prop) [decidable_pred p] [locally_finite_order_bot α] (a : subtype p) :
finset.Iio a = finset.subtype p (finset.Iio ↑a)
source
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) :
finset.map (function.embedding.subtype p) (finset.Iic a) = finset.Iic ↑a
source
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) :
finset.map (function.embedding.subtype p) (finset.Iio a) = finset.Iio ↑a