# 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 Mathlib.Order.Interval.Finset.Basic.

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

In a LocallyFiniteOrderTop,

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

In a LocallyFiniteOrderBot,

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

## 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 Order.Interval.Finset.Nat
• ℤ is in Data.Int.Interval
• ℕ+ is in Data.PNat.Interval
• Fin n is in Order.Interval.Finset.Fin
• 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
theorem LocallyFiniteOrder.finset_mem_Icc {α : Type u_1} [] [self : ] (a : α) (b : α) (x : α) :
a x x b

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

theorem LocallyFiniteOrder.finset_mem_Ico {α : Type u_1} [] [self : ] (a : α) (b : α) (x : α) :
a x x < b

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

theorem LocallyFiniteOrder.finset_mem_Ioc {α : Type u_1} [] [self : ] (a : α) (b : α) (x : α) :
a < x x b

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

theorem LocallyFiniteOrder.finset_mem_Ioo {α : Type u_1} [] [self : ] (a : α) (b : α) (x : α) :
a < x x < b

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

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
theorem LocallyFiniteOrderTop.finset_mem_Ici {α : Type u_1} [] [self : ] (a : α) (x : α) :
a x

x ∈ finsetIci a ↔ a ≤ x

theorem LocallyFiniteOrderTop.finset_mem_Ioi {α : Type u_1} [] [self : ] (a : α) (x : α) :
a < x

x ∈ finsetIoi a ↔ a < x

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
theorem LocallyFiniteOrderBot.finset_mem_Iic {α : Type u_1} [] [self : ] (a : α) (x : α) :
x a

x ∈ finsetIic a ↔ x ≤ a

theorem LocallyFiniteOrderBot.finset_mem_Iio {α : Type u_1} [] [self : ] (a : α) (x : α) :
x < a

x ∈ finsetIio a ↔ x < a

def LocallyFiniteOrder.ofIcc' (α : Type u_1) [] [DecidableRel fun (x1 x2 : α) => x1 x2] (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 (x1 x2 : α) => x1 x2] (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 (x1 x2 : α) => x1 x2] (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, inline]
abbrev 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, inline]
abbrev 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, inline]
abbrev 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 : α) :
(Finset.Icc a b) = Set.Icc a b
@[simp]
theorem Finset.coe_Ico {α : Type u_1} [] (a : α) (b : α) :
(Finset.Ico a b) = Set.Ico a b
@[simp]
theorem Finset.coe_Ioc {α : Type u_1} [] (a : α) (b : α) :
(Finset.Ioc a b) = Set.Ioc a b
@[simp]
theorem Finset.coe_Ioo {α : Type u_1} [] (a : α) (b : α) :
(Finset.Ioo 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 : α) :
(Finset.Ici a) =
@[simp]
theorem Finset.coe_Ioi {α : Type u_1} [] (a : α) :
(Finset.Ioi 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 : α) :
(Finset.Iic a) =
@[simp]
theorem Finset.coe_Iio {α : Type u_1} [] (a : α) :
(Finset.Iio a) =
@[instance 100]
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 : α) :
@[instance 100]
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 : α) :
(Finset.uIcc a b) = Set.uIcc a b

Elaborate set builder notation for Finset.

• {x ≤ a | p x} is elaborated as Finset.filter (fun x ↦ p x) (Finset.Iic a) if the expected type is Finset ?α.
• {x ≥ a | p x} is elaborated as Finset.filter (fun x ↦ p x) (Finset.Ici a) if the expected type is Finset ?α.
• {x < a | p x} is elaborated as Finset.filter (fun x ↦ p x) (Finset.Iio a) if the expected type is Finset ?α.
• {x > a | p x} is elaborated as Finset.filter (fun x ↦ p x) (Finset.Ioi a) if the expected type is Finset ?α.

• Data.Set.Defs for the Set builder notation elaborator that this elaborator partly overrides.
• Data.Finset.Basic for the Finset builder notation elaborator partly overriding this one for syntax of the form {x ∈ s | p x}.
• Data.Fintype.Basic for the Finset builder notation elaborator handling syntax of the form {x | p x}, {x : α | p x}, {x ∉ s | p x}, {x ≠ a | p x}.

TODO: Write a delaborator

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

### 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 : α) :
(Set.Icc a b).Finite
theorem Set.finite_Ico {α : Type u_1} [] (a : α) (b : α) :
(Set.Ico a b).Finite
theorem Set.finite_Ioc {α : Type u_1} [] (a : α) (b : α) :
(Set.Ioc a b).Finite
theorem Set.finite_Ioo {α : Type u_1} [] (a : α) (b : α) :
(Set.Ioo a b).Finite
instance Set.fintypeIci {α : Type u_1} [] (a : α) :
Equations
instance Set.fintypeIoi {α : Type u_1} [] (a : α) :
Equations
theorem Set.finite_Ici {α : Type u_1} [] (a : α) :
(Set.Ici a).Finite
theorem Set.finite_Ioi {α : Type u_1} [] (a : α) :
(Set.Ioi a).Finite
instance Set.fintypeIic {α : Type u_1} [] (b : α) :
Equations
instance Set.fintypeIio {α : Type u_1} [] (b : α) :
Equations
theorem Set.finite_Iic {α : Type u_1} [] (b : α) :
(Set.Iic b).Finite
theorem Set.finite_Iio {α : Type u_1} [] (b : α) :
(Set.Iio b).Finite
instance Set.fintypeUIcc {α : Type u_1} [] (a : α) (b : α) :
Fintype (Set.uIcc a b)
Equations
@[simp]
theorem Set.finite_interval {α : Type u_1} [] (a : α) (b : α) :
(Set.uIcc a b).Finite

### Instances #

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

A noncomputable constructor from the finiteness of all closed intervals.

Equations
Instances For
@[reducible, inline]
abbrev Fintype.toLocallyFiniteOrder {α : Type u_1} [] [] [DecidableRel fun (x1 x2 : α) => x1 < x2] [DecidableRel fun (x1 x2 : α) => x1 x2] :

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

### OrderDual#

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 Finset.Icc_toDual {α : Type u_1} [] (a : α) (b : α) :
Finset.Icc (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.Icc b a)
theorem Finset.Ico_toDual {α : Type u_1} [] (a : α) (b : α) :
Finset.Ico (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioc b a)
theorem Finset.Ioc_toDual {α : Type u_1} [] (a : α) (b : α) :
Finset.Ioc (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ico b a)
theorem Finset.Ioo_toDual {α : Type u_1} [] (a : α) (b : α) :
Finset.Ioo (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioo b a)
theorem Finset.Icc_ofDual {α : Type u_1} [] (a : αᵒᵈ) (b : αᵒᵈ) :
Finset.Icc (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Icc b a)
theorem Finset.Ico_ofDual {α : Type u_1} [] (a : αᵒᵈ) (b : αᵒᵈ) :
Finset.Ico (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ioc b a)
theorem Finset.Ioc_ofDual {α : Type u_1} [] (a : αᵒᵈ) (b : αᵒᵈ) :
Finset.Ioc (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ico b a)
theorem Finset.Ioo_ofDual {α : Type u_1} [] (a : αᵒᵈ) (b : αᵒᵈ) :
Finset.Ioo (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ioo b a)
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 Finset.Iic_toDual {α : Type u_1} [] (a : α) :
Finset.Iic (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ici a)
theorem Finset.Iio_toDual {α : Type u_1} [] (a : α) :
Finset.Iio (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioi a)
theorem Finset.Ici_ofDual {α : Type u_1} [] (a : αᵒᵈ) :
Finset.Ici (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Iic a)
theorem Finset.Ioi_ofDual {α : Type u_1} [] (a : αᵒᵈ) :
Finset.Ioi (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Iio a)
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 Finset.Ici_toDual {α : Type u_1} [] (a : α) :
Finset.Ici (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Iic a)
theorem Finset.Ioi_toDual {α : Type u_1} [] (a : α) :
Finset.Ioi (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Iio a)
theorem Finset.Iic_ofDual {α : Type u_1} [] (a : αᵒᵈ) :
Finset.Iic (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ici a)
theorem Finset.Iio_ofDual {α : Type u_1} [] (a : αᵒᵈ) :
Finset.Iio (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ioi a)

### Prod#

instance Prod.instLocallyFiniteOrder {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x1 x2 : α × β) => x1 x2] :
Equations
theorem Finset.Icc_prod_def {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x1 x2 : α × β) => x1 x2] (x : α × β) (y : α × β) :
= Finset.Icc x.1 y.1 ×ˢ Finset.Icc x.2 y.2
theorem Finset.Icc_product_Icc {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x1 x2 : α × β) => x1 x2] (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) :
Finset.Icc a₁ a₂ ×ˢ Finset.Icc b₁ b₂ = Finset.Icc (a₁, b₁) (a₂, b₂)
theorem Finset.card_Icc_prod {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x1 x2 : α × β) => x1 x2] (x : α × β) (y : α × β) :
(Finset.Icc x y).card = (Finset.Icc x.1 y.1).card * (Finset.Icc x.2 y.2).card
instance Prod.instLocallyFiniteOrderTop {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x1 x2 : α × β) => x1 x2] :
Equations
theorem Finset.Ici_prod_def {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x1 x2 : α × β) => x1 x2] (x : α × β) :
theorem Finset.Ici_product_Ici {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x1 x2 : α × β) => x1 x2] (a : α) (b : β) :
= Finset.Ici (a, b)
theorem Finset.card_Ici_prod {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x1 x2 : α × β) => x1 x2] (x : α × β) :
(Finset.Ici x).card = (Finset.Ici x.1).card * (Finset.Ici x.2).card
instance Prod.instLocallyFiniteOrderBot {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x1 x2 : α × β) => x1 x2] :
Equations
theorem Finset.Iic_prod_def {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x1 x2 : α × β) => x1 x2] (x : α × β) :
theorem Finset.Iic_product_Iic {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x1 x2 : α × β) => x1 x2] (a : α) (b : β) :
= Finset.Iic (a, b)
theorem Finset.card_Iic_prod {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x1 x2 : α × β) => x1 x2] (x : α × β) :
(Finset.Iic x).card = (Finset.Iic x.1).card * (Finset.Iic x.2).card
theorem Finset.uIcc_prod_def {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x1 x2 : α × β) => x1 x2] (x : α × β) (y : α × β) :
= Finset.uIcc x.1 y.1 ×ˢ Finset.uIcc x.2 y.2
theorem Finset.uIcc_product_uIcc {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x1 x2 : α × β) => x1 x2] (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) :
Finset.uIcc a₁ a₂ ×ˢ Finset.uIcc b₁ b₂ = Finset.uIcc (a₁, b₁) (a₂, b₂)
theorem Finset.card_uIcc_prod {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x1 x2 : α × β) => x1 x2] (x : α × β) (y : α × β) :
(Finset.uIcc x y).card = (Finset.uIcc x.1 y.1).card * (Finset.uIcc x.2 y.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 (Finset.Ici a)
theorem WithTop.Icc_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Icc a b = Finset.map Function.Embedding.some (Finset.Icc a b)
theorem WithTop.Ico_coe_top (α : Type u_1) [] [] (a : α) :
= Finset.map Function.Embedding.some (Finset.Ici a)
theorem WithTop.Ico_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Ico a b = Finset.map Function.Embedding.some (Finset.Ico a b)
theorem WithTop.Ioc_coe_top (α : Type u_1) [] [] (a : α) :
= Finset.insertNone (Finset.Ioi a)
theorem WithTop.Ioc_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Ioc a b = Finset.map Function.Embedding.some (Finset.Ioc a b)
theorem WithTop.Ioo_coe_top (α : Type u_1) [] [] (a : α) :
= Finset.map Function.Embedding.some (Finset.Ioi a)
theorem WithTop.Ioo_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Ioo a b = Finset.map Function.Embedding.some (Finset.Ioo a b)
instance WithBot.instLocallyFiniteOrder (α : Type u_1) [] [] :
Equations
• = OrderDual.instLocallyFiniteOrder
theorem WithBot.Icc_bot_coe (α : Type u_1) [] [] (b : α) :
= Finset.insertNone (Finset.Iic b)
theorem WithBot.Icc_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Icc a b = Finset.map Function.Embedding.some (Finset.Icc a b)
theorem WithBot.Ico_bot_coe (α : Type u_1) [] [] (b : α) :
= Finset.insertNone (Finset.Iio b)
theorem WithBot.Ico_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Ico a b = Finset.map Function.Embedding.some (Finset.Ico a b)
theorem WithBot.Ioc_bot_coe (α : Type u_1) [] [] (b : α) :
= Finset.map Function.Embedding.some (Finset.Iic b)
theorem WithBot.Ioc_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Ioc a b = Finset.map Function.Embedding.some (Finset.Ioc a b)
theorem WithBot.Ioo_bot_coe (α : Type u_1) [] [] (b : α) :
= Finset.map Function.Embedding.some (Finset.Iio b)
theorem WithBot.Ioo_coe_coe (α : Type u_1) [] [] (a : α) (b : α) :
Finset.Ioo a b = Finset.map Function.Embedding.some (Finset.Ioo a b)

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

@[reducible, inline]
abbrev 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, inline]
abbrev 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, inline]
abbrev 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₁ : ) :
s.Finite
theorem Set.finite_iff_bddAbove {α : Type u_3} {s : Set α} [] [] :
s.Finite
theorem Set.finite_iff_bddBelow {α : Type u_3} {s : Set α} [] [] :
s.Finite
theorem Set.finite_iff_bddBelow_bddAbove {α : Type u_3} {s : Set α} [] [] :
s.Finite

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

@[instance 100]
instance instLocallyFiniteOrderTopSubtypeLeOfDecidableRelOfLocallyFiniteOrder {α : Type u_1} {y : α} [] [DecidableRel fun (x1 x2 : α) => x1 x2] :
LocallyFiniteOrderTop { x : α // x y }
Equations
• One or more equations did not get rendered due to their size.
@[instance 100]
instance instLocallyFiniteOrderTopSubtypeLtOfDecidableRelOfLocallyFiniteOrder {α : Type u_1} {y : α} [] [DecidableRel fun (x1 x2 : α) => x1 < x2] :
LocallyFiniteOrderTop { x : α // x < y }
Equations
• One or more equations did not get rendered due to their size.
@[instance 100]
instance instLocallyFiniteOrderBotSubtypeLeOfDecidableRelOfLocallyFiniteOrder {α : Type u_1} {y : α} [] [DecidableRel fun (x1 x2 : α) => x1 x2] :
LocallyFiniteOrderBot { x : α // y x }
Equations
• One or more equations did not get rendered due to their size.
@[instance 100]
instance instLocallyFiniteOrderBotSubtypeLtOfDecidableRelOfLocallyFiniteOrder {α : Type u_1} {y : α} [] [DecidableRel fun (x1 x2 : α) => x1 < x2] :
LocallyFiniteOrderBot { x : α // y < x }
Equations
• One or more equations did not get rendered due to their size.
instance instFiniteSubtypeLeOfLocallyFiniteOrderBot {α : Type u_1} {y : α} [] :
Finite { x : α // x y }
Equations
• =
instance instFiniteSubtypeLtOfLocallyFiniteOrderBot {α : Type u_1} {y : α} [] :
Finite { x : α // x < y }
Equations
• =
instance instFiniteSubtypeLeOfLocallyFiniteOrderTop {α : Type u_1} {y : α} [] :
Finite { x : α // y x }
Equations
• =
instance instFiniteSubtypeLtOfLocallyFiniteOrderTop {α : Type u_1} {y : α} [] :
Finite { x : α // y < x }
Equations
• =
@[simp]
theorem Set.toFinset_Icc {α : Type u_3} [] (a : α) (b : α) [Fintype (Set.Icc a b)] :
(Set.Icc a b).toFinset =
@[simp]
theorem Set.toFinset_Ico {α : Type u_3} [] (a : α) (b : α) [Fintype (Set.Ico a b)] :
(Set.Ico a b).toFinset =
@[simp]
theorem Set.toFinset_Ioc {α : Type u_3} [] (a : α) (b : α) [Fintype (Set.Ioc a b)] :
(Set.Ioc a b).toFinset =
@[simp]
theorem Set.toFinset_Ioo {α : Type u_3} [] (a : α) (b : α) [Fintype (Set.Ioo a b)] :
(Set.Ioo a b).toFinset =
@[simp]
theorem Set.toFinset_Ici {α : Type u_3} [] (a : α) [Fintype (Set.Ici a)] :
(Set.Ici a).toFinset =
@[simp]
theorem Set.toFinset_Ioi {α : Type u_3} [] (a : α) [Fintype (Set.Ioi a)] :
(Set.Ioi a).toFinset =
@[simp]
theorem Set.toFinset_Iic {α : Type u_3} [] (a : α) [Fintype (Set.Iic a)] :
(Set.Iic a).toFinset =
@[simp]
theorem Set.toFinset_Iio {α : Type u_3} [] (a : α) [Fintype (Set.Iio a)] :
(Set.Iio a).toFinset =