# 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.LocallyFinite.

## 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 LocallyFiniteOrder,

• 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.
• Finset.uIcc: Unordered closed 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.

In a LocallyFiniteOrderTop,

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

In a LocallyFiniteOrderBot,

• 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 LocallyFiniteOrder instance can be built

• for a subtype of a locally finite order. See Subtype.locallyFiniteOrder.
• for the product of two locally finite orders. See Prod.locallyFiniteOrder.
• for any fintype (but not as an instance). See Fintype.toLocallyFiniteOrder.
• from a definition of Finset.Icc alone. See LocallyFiniteOrder.ofIcc.
• by pulling back LocallyFiniteOrder β through an order embedding f : α →o β. See OrderEmbedding.locallyFiniteOrder.

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
• Σ i, α i is in Data.Sigma.Interval Along, you will find lemmas about the cardinality of those finite intervals.

## TODO #

Provide the LocallyFiniteOrder instance for α ×ₗ β where LocallyFiniteOrder α and Fintype β.

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

From LinearOrder α, NoMaxOrder α, LocallyFiniteOrder α, we can also define an order isomorphism α ≃ ℕ or α ≃ ℤ, depending on whether we have OrderBot α or NoMinOrder α and Nonempty α. When OrderBot α, we can match a : α to (Iio a).card.

We can provide SuccOrder α from LinearOrder α and LocallyFiniteOrder α using

lemma exists_min_greater [LinearOrder α] [LocallyFiniteOrder α] {x ub : α} (hx : x < ub) :
∃ lub, x < lub ∧ ∀ y, x < y → lub ≤ y := by
-- very non golfed
have h : (Finset.Ioc x ub).Nonempty := ⟨ub, Finset.mem_Ioc.2 ⟨hx, le_rfl⟩⟩
use Finset.min' (Finset.Ioc x ub) h
constructor
· exact (Finset.mem_Ioc.mp <| Finset.min'_mem _ h).1
rintro y hxy
obtain hy | hy := le_total y ub
· refine Finset.min'_le (Ioc x ub) y ?_
simp [*] at *
· exact (Finset.min'_le _ _ (Finset.mem_Ioc.2 ⟨hx, le_rfl⟩)).trans hy


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 SuccOrder, but it's not locally finite as Icc (-1) 1 is infinite.

class LocallyFiniteOrder (α : Type u_1) [] :
Type u_1

This is a mixin class describing a locally finite order, that is, is an order where bounded intervals are finite. When you don't care too much about definitional equality, you can use LocallyFiniteOrder.ofIcc or LocallyFiniteOrder.ofFiniteIcc to build a locally finite order from just Finset.Icc.

• finsetIcc : αα

Left-closed right-closed interval

• finsetIco : αα

Left-closed right-open interval

• finsetIoc : αα

Left-open right-closed interval

• finsetIoo : αα

Left-open right-open interval

• finset_mem_Icc : ∀ (a b x : α), a x x b

x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b

• finset_mem_Ico : ∀ (a b x : α), a x x < b

x ∈ finsetIco a b ↔ a ≤ x ∧ x < b

• finset_mem_Ioc : ∀ (a b x : α), a < x x b

x ∈ finsetIoc a b ↔ a < x ∧ x ≤ b

• finset_mem_Ioo : ∀ (a b x : α), a < x x < b

x ∈ finsetIoo a b ↔ a < x ∧ x < b

Instances
class LocallyFiniteOrderTop (α : Type u_1) [] :
Type u_1

This mixin class describes an order where all intervals bounded below are finite. This is slightly weaker than LocallyFiniteOrder + OrderTop as it allows empty types.

• finsetIoi : α

Left-open right-infinite interval

• finsetIci : α

Left-closed right-infinite interval

• finset_mem_Ici : ∀ (a x : α), a x

x ∈ finsetIci a ↔ a ≤ x

• finset_mem_Ioi : ∀ (a x : α), a < x

x ∈ finsetIoi a ↔ a < x

Instances
class LocallyFiniteOrderBot (α : Type u_1) [] :
Type u_1

This mixin class describes an order where all intervals bounded above are finite. This is slightly weaker than LocallyFiniteOrder + OrderBot as it allows empty types.

• finsetIio : α

Left-infinite right-open interval

• finsetIic : α

Left-infinite right-closed interval

• finset_mem_Iic : ∀ (a x : α), x a

x ∈ finsetIic a ↔ x ≤ a

• finset_mem_Iio : ∀ (a x : α), x < a

x ∈ finsetIio a ↔ x < a

Instances
def LocallyFiniteOrder.ofIcc' (α : Type u_1) [] [DecidableRel fun (x x_1 : α) => x x_1] (finsetIcc : αα) (mem_Icc : ∀ (a b x : α), x finsetIcc 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 LocallyFiniteOrder.ofIcc, this one requires DecidableRel (· ≤ ·) but only Preorder.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def LocallyFiniteOrder.ofIcc (α : Type u_1) [] [] (finsetIcc : αα) (mem_Icc : ∀ (a b x : α), x finsetIcc 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 LocallyFiniteOrder.ofIcc', this one requires PartialOrder but only DecidableEq.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def LocallyFiniteOrderTop.ofIci' (α : Type u_1) [] [DecidableRel fun (x x_1 : α) => x x_1] (finsetIci : α) (mem_Ici : ∀ (a x : α), x finsetIci a a x) :

A constructor from a definition of Finset.Ici alone, the other ones being derived by removing the ends. As opposed to LocallyFiniteOrderTop.ofIci, this one requires DecidableRel (· ≤ ·) but only Preorder.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def LocallyFiniteOrderTop.ofIci (α : Type u_1) [] [] (finsetIci : α) (mem_Ici : ∀ (a x : α), x finsetIci a a x) :

A constructor from a definition of Finset.Ici alone, the other ones being derived by removing the ends. As opposed to LocallyFiniteOrderTop.ofIci', this one requires PartialOrder but only DecidableEq.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def LocallyFiniteOrderBot.ofIic' (α : Type u_1) [] [DecidableRel fun (x x_1 : α) => x x_1] (finsetIic : α) (mem_Iic : ∀ (a x : α), x finsetIic a x a) :

A constructor from a definition of Finset.Iic alone, the other ones being derived by removing the ends. As opposed to LocallyFiniteOrderBot.ofIic, this one requires DecidableRel (· ≤ ·) but only Preorder.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def LocallyFiniteOrderBot.ofIic (α : Type u_1) [] [] (finsetIic : α) (mem_Iic : ∀ (a x : α), x finsetIic a x a) :

A constructor from a definition of Finset.Iic alone, the other ones being derived by removing the ends. As opposed to LocallyFiniteOrderBot.ofIic', this one requires PartialOrder but only DecidableEq.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def IsEmpty.toLocallyFiniteOrder {α : Type u_1} [] [] :

An empty type is locally finite.

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def IsEmpty.toLocallyFiniteOrderTop {α : Type u_1} [] [] :

An empty type is locally finite.

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

Equations
• IsEmpty.toLocallyFiniteOrderTop = { finsetIoi := fun (a : α) => , finsetIci := fun (a : α) => , finset_mem_Ici := , finset_mem_Ioi := }
Instances For
@[reducible]
def IsEmpty.toLocallyFiniteOrderBot {α : Type u_1} [] [] :

An empty type is locally finite.

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

Equations
• IsEmpty.toLocallyFiniteOrderBot = { finsetIio := fun (a : α) => , finsetIic := fun (a : α) => , finset_mem_Iic := , finset_mem_Iio := }
Instances For

### Intervals as finsets #

def Finset.Icc {α : Type u_1} [] (a : α) (b : α) :

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

Equations
Instances For
def Finset.Ico {α : Type u_1} [] (a : α) (b : α) :

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

Equations
Instances For
def Finset.Ioc {α : Type u_1} [] (a : α) (b : α) :

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

Equations
Instances For
def Finset.Ioo {α : Type u_1} [] (a : α) (b : α) :

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

Equations
Instances For
@[simp]
theorem Finset.mem_Icc {α : Type u_1} [] {a : α} {b : α} {x : α} :
x a x x b
@[simp]
theorem Finset.mem_Ico {α : Type u_1} [] {a : α} {b : α} {x : α} :
x a x x < b
@[simp]
theorem Finset.mem_Ioc {α : Type u_1} [] {a : α} {b : α} {x : α} :
x a < x x b
@[simp]
theorem Finset.mem_Ioo {α : Type u_1} [] {a : α} {b : α} {x : α} :
x a < x x < b
@[simp]
theorem Finset.coe_Icc {α : Type u_1} [] (a : α) (b : α) :
() = Set.Icc a b
@[simp]
theorem Finset.coe_Ico {α : Type u_1} [] (a : α) (b : α) :
() = Set.Ico a b
@[simp]
theorem Finset.coe_Ioc {α : Type u_1} [] (a : α) (b : α) :
() = Set.Ioc a b
@[simp]
theorem Finset.coe_Ioo {α : Type u_1} [] (a : α) (b : α) :
() = Set.Ioo a b
def Finset.Ici {α : Type u_1} [] (a : α) :

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

Equations
Instances For
def Finset.Ioi {α : Type u_1} [] (a : α) :

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

Equations
Instances For
@[simp]
theorem Finset.mem_Ici {α : Type u_1} [] {a : α} {x : α} :
x a x
@[simp]
theorem Finset.mem_Ioi {α : Type u_1} [] {a : α} {x : α} :
x a < x
@[simp]
theorem Finset.coe_Ici {α : Type u_1} [] (a : α) :
() =
@[simp]
theorem Finset.coe_Ioi {α : Type u_1} [] (a : α) :
() =
def Finset.Iic {α : Type u_1} [] (a : α) :

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

Equations
Instances For
def Finset.Iio {α : Type u_1} [] (a : α) :

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

Equations
Instances For
@[simp]
theorem Finset.mem_Iic {α : Type u_1} [] {a : α} {x : α} :
x x a
@[simp]
theorem Finset.mem_Iio {α : Type u_1} [] {a : α} {x : α} :
x x < a
@[simp]
theorem Finset.coe_Iic {α : Type u_1} [] (a : α) :
() =
@[simp]
theorem Finset.coe_Iio {α : Type u_1} [] (a : α) :
() =
Equations
• LocallyFiniteOrder.toLocallyFiniteOrderTop = { finsetIoi := fun (b : α) => , finsetIci := fun (b : α) => , finset_mem_Ici := , finset_mem_Ioi := }
theorem Finset.Ici_eq_Icc {α : Type u_1} [] [] (a : α) :
theorem Finset.Ioi_eq_Ioc {α : Type u_1} [] [] (a : α) :
Equations
• Finset.LocallyFiniteOrder.toLocallyFiniteOrderBot = { finsetIio := , finsetIic := , finset_mem_Iic := , finset_mem_Iio := }
theorem Finset.Iic_eq_Icc {α : Type u_1} [] [] :
Finset.Iic =
theorem Finset.Iio_eq_Ico {α : Type u_1} [] [] :
Finset.Iio =
def Finset.uIcc {α : Type u_1} [] (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
Instances For

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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Finset.mem_uIcc {α : Type u_1} [] {a : α} {b : α} {x : α} :
x a b x x a b
@[simp]
theorem Finset.coe_uIcc {α : Type u_1} [] (a : α) (b : α) :
() = Set.uIcc a b

### Intervals as multisets #

def Multiset.Icc {α : Type u_1} [] (a : α) (b : α) :

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

Equations
• = ().val
Instances For
def Multiset.Ico {α : Type u_1} [] (a : α) (b : α) :

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

Equations
• = ().val
Instances For
def Multiset.Ioc {α : Type u_1} [] (a : α) (b : α) :

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

Equations
• = ().val
Instances For
def Multiset.Ioo {α : Type u_1} [] (a : α) (b : α) :

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

Equations
• = ().val
Instances For
@[simp]
theorem Multiset.mem_Icc {α : Type u_1} [] {a : α} {b : α} {x : α} :
x a x x b
@[simp]
theorem Multiset.mem_Ico {α : Type u_1} [] {a : α} {b : α} {x : α} :
x a x x < b
@[simp]
theorem Multiset.mem_Ioc {α : Type u_1} [] {a : α} {b : α} {x : α} :
x a < x x b
@[simp]
theorem Multiset.mem_Ioo {α : Type u_1} [] {a : α} {b : α} {x : α} :
x a < x x < b
def Multiset.Ici {α : Type u_1} [] (a : α) :

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

Equations
• = ().val
Instances For
def Multiset.Ioi {α : Type u_1} [] (a : α) :

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

Equations
• = ().val
Instances For
@[simp]
theorem Multiset.mem_Ici {α : Type u_1} [] {a : α} {x : α} :
a x
@[simp]
theorem Multiset.mem_Ioi {α : Type u_1} [] {a : α} {x : α} :
a < x
def Multiset.Iic {α : Type u_1} [] (b : α) :

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

Equations
• = ().val
Instances For
def Multiset.Iio {α : Type u_1} [] (b : α) :

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

Equations
• = ().val
Instances For
@[simp]
theorem Multiset.mem_Iic {α : Type u_1} [] {b : α} {x : α} :
x b
@[simp]
theorem Multiset.mem_Iio {α : Type u_1} [] {b : α} {x : α} :
x < b

### Finiteness of Set intervals #

instance Set.fintypeIcc {α : Type u_1} [] (a : α) (b : α) :
Fintype (Set.Icc a b)
Equations
instance Set.fintypeIco {α : Type u_1} [] (a : α) (b : α) :
Fintype (Set.Ico a b)
Equations
instance Set.fintypeIoc {α : Type u_1} [] (a : α) (b : α) :
Fintype (Set.Ioc a b)
Equations
instance Set.fintypeIoo {α : Type u_1} [] (a : α) (b : α) :
Fintype (Set.Ioo a b)
Equations
theorem Set.finite_Icc {α : Type u_1} [] (a : α) (b : α) :
theorem Set.finite_Ico {α : Type u_1} [] (a : α) (b : α) :
theorem Set.finite_Ioc {α : Type u_1} [] (a : α) (b : α) :
theorem Set.finite_Ioo {α : Type u_1} [] (a : α) (b : α) :
instance Set.fintypeIci {α : Type u_1} [] (a : α) :
Fintype ()
Equations
instance Set.fintypeIoi {α : Type u_1} [] (a : α) :
Fintype ()
Equations
theorem Set.finite_Ici {α : Type u_1} [] (a : α) :
theorem Set.finite_Ioi {α : Type u_1} [] (a : α) :
instance Set.fintypeIic {α : Type u_1} [] (b : α) :
Fintype ()
Equations
instance Set.fintypeIio {α : Type u_1} [] (b : α) :
Fintype ()
Equations
theorem Set.finite_Iic {α : Type u_1} [] (b : α) :
theorem Set.finite_Iio {α : Type u_1} [] (b : α) :
instance Set.fintypeUIcc {α : Type u_1} [] (a : α) (b : α) :
Fintype (Set.uIcc a b)
Equations
@[simp]
theorem Set.finite_interval {α : Type u_1} [] (a : α) (b : α) :

### Instances #

noncomputable def LocallyFiniteOrder.ofFiniteIcc {α : Type u_1} [] (h : ∀ (a b : α), Set.Finite (Set.Icc a b)) :

A noncomputable constructor from the finiteness of all closed intervals.

Equations
Instances For
@[reducible]
def Fintype.toLocallyFiniteOrder {α : Type u_1} [] [] [DecidableRel fun (x x_1 : α) => x < x_1] [DecidableRel fun (x x_1 : α) => x x_1] :

A fintype is a locally finite order.

This is not an instance as it would not be defeq to better instances such as Fin.locallyFiniteOrder.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance instSubsingletonLocallyFiniteOrder {α : Type u_1} [] :
Equations
• =
Equations
• =
Equations
• =
noncomputable def OrderEmbedding.locallyFiniteOrder {α : Type u_1} {β : Type u_2} [] [] (f : α ↪o β) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance OrderDual.instLocallyFiniteOrder {α : Type u_1} [] :

Note we define Icc (toDual a) (toDual b) as Icc α _ _ b a (which has type Finset α not Finset αᵒᵈ!) instead of (Icc b a).map toDual.toEmbedding as this means the following is defeq:

lemma this : (Icc (toDual (toDual a)) (toDual (toDual b)) : _) = (Icc a b : _) := rfl

Equations
• One or more equations did not get rendered due to their size.
theorem Icc_toDual {α : Type u_1} [] (a : α) (b : α) :
Finset.Icc (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map (Equiv.toEmbedding OrderDual.toDual) ()
theorem Ico_toDual {α : Type u_1} [] (a : α) (b : α) :
Finset.Ico (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map (Equiv.toEmbedding OrderDual.toDual) ()
theorem Ioc_toDual {α : Type u_1} [] (a : α) (b : α) :
Finset.Ioc (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map (Equiv.toEmbedding OrderDual.toDual) ()
theorem Ioo_toDual {α : Type u_1} [] (a : α) (b : α) :
Finset.Ioo (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map (Equiv.toEmbedding OrderDual.toDual) ()
theorem Icc_ofDual {α : Type u_1} [] (a : αᵒᵈ) (b : αᵒᵈ) :
Finset.Icc (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) ()
theorem Ico_ofDual {α : Type u_1} [] (a : αᵒᵈ) (b : αᵒᵈ) :
Finset.Ico (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) ()
theorem Ioc_ofDual {α : Type u_1} [] (a : αᵒᵈ) (b : αᵒᵈ) :
Finset.Ioc (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) ()
theorem Ioo_ofDual {α : Type u_1} [] (a : αᵒᵈ) (b : αᵒᵈ) :
Finset.Ioo (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) ()
instance OrderDual.instLocallyFiniteOrderBot {α : Type u_1} [] :

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

lemma this : (Iic (toDual (toDual a)) : _) = (Iic a : _) := rfl

Equations
• One or more equations did not get rendered due to their size.
theorem Iic_toDual {α : Type u_1} [] (a : α) :
Finset.Iic (OrderDual.toDual a) = Finset.map (Equiv.toEmbedding OrderDual.toDual) ()
theorem Iio_toDual {α : Type u_1} [] (a : α) :
Finset.Iio (OrderDual.toDual a) = Finset.map (Equiv.toEmbedding OrderDual.toDual) ()
theorem Ici_ofDual {α : Type u_1} [] (a : αᵒᵈ) :
Finset.Ici (OrderDual.ofDual a) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) ()
theorem Ioi_ofDual {α : Type u_1} [] (a : αᵒᵈ) :
Finset.Ioi (OrderDual.ofDual a) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) ()
instance OrderDual.instLocallyFiniteOrderTop {α : Type u_1} [] :

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

lemma this : (Ici (toDual (toDual a)) : _) = (Ici a : _) := rfl

Equations
• One or more equations did not get rendered due to their size.
theorem Ici_toDual {α : Type u_1} [] (a : α) :
Finset.Ici (OrderDual.toDual a) = Finset.map (Equiv.toEmbedding OrderDual.toDual) ()
theorem Ioi_toDual {α : Type u_1} [] (a : α) :
Finset.Ioi (OrderDual.toDual a) = Finset.map (Equiv.toEmbedding OrderDual.toDual) ()
theorem Iic_ofDual {α : Type u_1} [] (a : αᵒᵈ) :
Finset.Iic (OrderDual.ofDual a) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) ()
theorem Iio_ofDual {α : Type u_1} [] (a : αᵒᵈ) :
Finset.Iio (OrderDual.ofDual a) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) ()
instance Prod.instLocallyFiniteOrderProdInstPreorderProd {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x x_1 : α × β) => x x_1] :
Equations
instance Prod.instLocallyFiniteOrderTopProdInstPreorderProd {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x x_1 : α × β) => x x_1] :
Equations
instance Prod.instLocallyFiniteOrderBotProdInstPreorderProd {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x x_1 : α × β) => x x_1] :
Equations
theorem Prod.Icc_eq {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x x_1 : α × β) => x x_1] (p : α × β) (q : α × β) :
= Finset.Icc p.1 q.1 ×ˢ Finset.Icc p.2 q.2
@[simp]
theorem Prod.Icc_mk_mk {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x x_1 : α × β) => x x_1] (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} [] [] [DecidableRel fun (x x_1 : α × β) => x x_1] (p : α × β) (q : α × β) :
().card = (Finset.Icc p.1 q.1).card * (Finset.Icc p.2 q.2).card
theorem Prod.uIcc_eq {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x x_1 : α × β) => x x_1] (p : α × β) (q : α × β) :
= Finset.uIcc p.1 q.1 ×ˢ Finset.uIcc p.2 q.2
@[simp]
theorem Prod.uIcc_mk_mk {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x x_1 : α × β) => x x_1] (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} [] [] [DecidableRel fun (x x_1 : α × β) => x x_1] (p : α × β) (q : α × β) :
().card = (Finset.uIcc p.1 q.1).card * (Finset.uIcc p.2 q.2).card

#### WithTop, WithBot#

Adding a ⊤ to a locally finite OrderTop keeps it locally finite. Adding a ⊥ to a locally finite OrderBot keeps it locally finite.

instance WithTop.locallyFiniteOrder (α : Type u_1) [] [] :
Equations
• One or more equations did not get rendered due to their size.
theorem WithTop.Icc_coe_top (α : Type u_1) [] [] (a : α) :
= Finset.insertNone ()
theorem WithTop.Icc_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Icc a b = Finset.map Function.Embedding.some ()
theorem WithTop.Ico_coe_top (α : Type u_1) [] [] (a : α) :
= Finset.map Function.Embedding.some ()
theorem WithTop.Ico_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Ico a b = Finset.map Function.Embedding.some ()
theorem WithTop.Ioc_coe_top (α : Type u_1) [] [] (a : α) :
= Finset.insertNone ()
theorem WithTop.Ioc_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Ioc a b = Finset.map Function.Embedding.some ()
theorem WithTop.Ioo_coe_top (α : Type u_1) [] [] (a : α) :
= Finset.map Function.Embedding.some ()
theorem WithTop.Ioo_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Ioo a b = Finset.map Function.Embedding.some ()
instance WithBot.instLocallyFiniteOrder (α : Type u_1) [] [] :
Equations
• = OrderDual.instLocallyFiniteOrder
theorem WithBot.Icc_bot_coe (α : Type u_1) [] [] (b : α) :
= Finset.insertNone ()
theorem WithBot.Icc_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Icc a b = Finset.map Function.Embedding.some ()
theorem WithBot.Ico_bot_coe (α : Type u_1) [] [] (b : α) :
= Finset.insertNone ()
theorem WithBot.Ico_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Ico a b = Finset.map Function.Embedding.some ()
theorem WithBot.Ioc_bot_coe (α : Type u_1) [] [] (b : α) :
= Finset.map Function.Embedding.some ()
theorem WithBot.Ioc_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Ioc a b = Finset.map Function.Embedding.some ()
theorem WithBot.Ioo_bot_coe (α : Type u_1) [] [] (b : α) :
= Finset.map Function.Embedding.some ()
theorem WithBot.Ioo_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Ioo a b = Finset.map Function.Embedding.some ()

#### Transfer locally finite orders across order isomorphisms #

@[reducible]
def OrderIso.locallyFiniteOrder {α : Type u_1} {β : Type u_2} [] [] (f : α ≃o β) :

Transfer LocallyFiniteOrder across an OrderIso.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def OrderIso.locallyFiniteOrderTop {α : Type u_1} {β : Type u_2} [] [] (f : α ≃o β) :

Transfer LocallyFiniteOrderTop across an OrderIso.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def OrderIso.locallyFiniteOrderBot {α : Type u_1} {β : Type u_2} [] [] (f : α ≃o β) :

Transfer LocallyFiniteOrderBot across an OrderIso.

Equations
• One or more equations did not get rendered due to their size.
Instances For

#### Subtype of a locally finite order #

instance Subtype.instLocallyFiniteOrder {α : Type u_1} [] (p : αProp) [] :
Equations
• One or more equations did not get rendered due to their size.
instance Subtype.instLocallyFiniteOrderTop {α : Type u_1} [] (p : αProp) [] :
Equations
• One or more equations did not get rendered due to their size.
instance Subtype.instLocallyFiniteOrderBot {α : Type u_1} [] (p : αProp) [] :
Equations
• One or more equations did not get rendered due to their size.
theorem Finset.subtype_Icc_eq {α : Type u_1} [] (p : αProp) [] (a : ) (b : ) :
= Finset.subtype p (Finset.Icc a b)
theorem Finset.subtype_Ico_eq {α : Type u_1} [] (p : αProp) [] (a : ) (b : ) :
= Finset.subtype p (Finset.Ico a b)
theorem Finset.subtype_Ioc_eq {α : Type u_1} [] (p : αProp) [] (a : ) (b : ) :
= Finset.subtype p (Finset.Ioc a b)
theorem Finset.subtype_Ioo_eq {α : Type u_1} [] (p : αProp) [] (a : ) (b : ) :
= Finset.subtype p (Finset.Ioo a b)
theorem Finset.map_subtype_embedding_Icc {α : Type u_1} [] (p : αProp) [] (a : ) (b : ) (hp : ∀ ⦃a b x : α⦄, a xx bp ap bp x) :
= Finset.Icc a b
theorem Finset.map_subtype_embedding_Ico {α : Type u_1} [] (p : αProp) [] (a : ) (b : ) (hp : ∀ ⦃a b x : α⦄, a xx bp ap bp x) :
= Finset.Ico a b
theorem Finset.map_subtype_embedding_Ioc {α : Type u_1} [] (p : αProp) [] (a : ) (b : ) (hp : ∀ ⦃a b x : α⦄, a xx bp ap bp x) :
= Finset.Ioc a b
theorem Finset.map_subtype_embedding_Ioo {α : Type u_1} [] (p : αProp) [] (a : ) (b : ) (hp : ∀ ⦃a b x : α⦄, a xx bp ap bp x) :
= Finset.Ioo a b
theorem Finset.subtype_Ici_eq {α : Type u_1} [] (p : αProp) [] (a : ) :
theorem Finset.subtype_Ioi_eq {α : Type u_1} [] (p : αProp) [] (a : ) :
theorem Finset.map_subtype_embedding_Ici {α : Type u_1} [] (p : αProp) [] (a : ) (hp : ∀ ⦃a x : α⦄, a xp ap x) :
theorem Finset.map_subtype_embedding_Ioi {α : Type u_1} [] (p : αProp) [] (a : ) (hp : ∀ ⦃a x : α⦄, a xp ap x) :
theorem Finset.subtype_Iic_eq {α : Type u_1} [] (p : αProp) [] (a : ) :
theorem Finset.subtype_Iio_eq {α : Type u_1} [] (p : αProp) [] (a : ) :
theorem Finset.map_subtype_embedding_Iic {α : Type u_1} [] (p : αProp) [] (a : ) (hp : ∀ ⦃a x : α⦄, x ap ap x) :
theorem Finset.map_subtype_embedding_Iio {α : Type u_1} [] (p : αProp) [] (a : ) (hp : ∀ ⦃a x : α⦄, x ap ap x) :
theorem BddBelow.finite_of_bddAbove {α : Type u_3} [] {s : Set α} (h₀ : ) (h₁ : ) :
theorem Set.finite_iff_bddAbove {α : Type u_3} {s : Set α} [] [] :
theorem Set.finite_iff_bddBelow {α : Type u_3} {s : Set α} [] [] :
theorem Set.finite_iff_bddBelow_bddAbove {α : Type u_3} {s : Set α} [] [] :

We make the instances below low priority so when alternative constructions are available they are preferred.

instance instLocallyFiniteOrderTopSubtypeLeToLEPreorder {α : Type u_1} {y : α} [] [DecidableRel fun (x x_1 : α) => x x_1] :
LocallyFiniteOrderTop { x : α // x y }
Equations
• One or more equations did not get rendered due to their size.
instance instLocallyFiniteOrderTopSubtypeLtToLTPreorder {α : Type u_1} {y : α} [] [DecidableRel fun (x x_1 : α) => x < x_1] :
LocallyFiniteOrderTop { x : α // x < y }
Equations
• One or more equations did not get rendered due to their size.
instance instLocallyFiniteOrderBotSubtypeLeToLEPreorder {α : Type u_1} {y : α} [] [DecidableRel fun (x x_1 : α) => x x_1] :
LocallyFiniteOrderBot { x : α // y x }
Equations
• One or more equations did not get rendered due to their size.
instance instLocallyFiniteOrderBotSubtypeLtToLTPreorder {α : Type u_1} {y : α} [] [DecidableRel fun (x x_1 : α) => x < x_1] :
LocallyFiniteOrderBot { x : α // y < x }
Equations
• One or more equations did not get rendered due to their size.
instance instFiniteSubtypeLeToLE {α : Type u_1} {y : α} [] :
Finite { x : α // x y }
Equations
• =
instance instFiniteSubtypeLtToLT {α : Type u_1} {y : α} [] :
Finite { x : α // x < y }
Equations
• =
instance instFiniteSubtypeLeToLE_1 {α : Type u_1} {y : α} [] :
Finite { x : α // y x }
Equations
• =
instance instFiniteSubtypeLtToLT_1 {α : Type u_1} {y : α} [] :
Finite { x : α // y < x }
Equations
• =
@[simp]
theorem Set.toFinset_Icc {α : Type u_3} [] (a : α) (b : α) [Fintype (Set.Icc a b)] :
@[simp]
theorem Set.toFinset_Ico {α : Type u_3} [] (a : α) (b : α) [Fintype (Set.Ico a b)] :
@[simp]
theorem Set.toFinset_Ioc {α : Type u_3} [] (a : α) (b : α) [Fintype (Set.Ioc a b)] :
@[simp]
theorem Set.toFinset_Ioo {α : Type u_3} [] (a : α) (b : α) [Fintype (Set.Ioo a b)] :
@[simp]
theorem Set.toFinset_Ici {α : Type u_3} [] (a : α) [Fintype ()] :
@[simp]
theorem Set.toFinset_Ioi {α : Type u_3} [] (a : α) [Fintype ()] :
@[simp]
theorem Set.toFinset_Iic {α : Type u_3} [] (a : α) [Fintype ()] :
@[simp]
theorem Set.toFinset_Iio {α : Type u_3} [] (a : α) [Fintype ()] :