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

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) [Preorder α] : 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 : α → α → Finset α

  Left-closed right-closed interval

• finsetIco : α → α → Finset α

  Left-closed right-open interval

• finsetIoc : α → α → Finset α

  Left-open right-closed interval

• finsetIoo : α → α → Finset α

  Left-open right-open interval

• finset_mem_Icc : ∀ (a b x : α), x ∈ LocallyFiniteOrder.finsetIcc a b ↔ a ≤ x ∧ x ≤ b

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

• finset_mem_Ico : ∀ (a b x : α), x ∈ LocallyFiniteOrder.finsetIco a b ↔ a ≤ x ∧ x < b

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

• finset_mem_Ioc : ∀ (a b x : α), x ∈ LocallyFiniteOrder.finsetIoc a b ↔ a < x ∧ x ≤ b

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

• finset_mem_Ioo : ∀ (a b x : α), x ∈ LocallyFiniteOrder.finsetIoo a b ↔ a < x ∧ x < b

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

class LocallyFiniteOrderTop (α : Type u_1) [Preorder α] : 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 : α → Finset α

  Left-open right-infinite interval

• finsetIci : α → Finset α

  Left-closed right-infinite interval

• finset_mem_Ici : ∀ (a x : α), x ∈ LocallyFiniteOrderTop.finsetIci a ↔ a ≤ x

  x ∈ finsetIci a ↔ a ≤ x

• finset_mem_Ioi : ∀ (a x : α), x ∈ LocallyFiniteOrderTop.finsetIoi a ↔ a < x

  x ∈ finsetIoi a ↔ a < x

class LocallyFiniteOrderBot (α : Type u_1) [Preorder α] : 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 : α → Finset α

  Left-infinite right-open interval

• finsetIic : α → Finset α

  Left-infinite right-closed interval

• finset_mem_Iic : ∀ (a x : α), x ∈ LocallyFiniteOrderBot.finsetIic a ↔ x ≤ a

  x ∈ finsetIic a ↔ x ≤ a

• finset_mem_Iio : ∀ (a x : α), x ∈ LocallyFiniteOrderBot.finsetIio a ↔ x < a

  x ∈ finsetIio a ↔ x < a

def LocallyFiniteOrder.ofIcc' (α : Type u_1) [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (finsetIcc : α → α → Finset α) (mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b) : LocallyFiniteOrder α

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.

def LocallyFiniteOrder.ofIcc (α : Type u_1) [PartialOrder α] [DecidableEq α] (finsetIcc : α → α → Finset α) (mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b) : LocallyFiniteOrder α

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.

def LocallyFiniteOrderTop.ofIci' (α : Type u_1) [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (finsetIci : α → Finset α) (mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x) : LocallyFiniteOrderTop α

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.

def LocallyFiniteOrderTop.ofIci (α : Type u_1) [PartialOrder α] [DecidableEq α] (finsetIci : α → Finset α) (mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x) : LocallyFiniteOrderTop α

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.

def LocallyFiniteOrderBot.ofIic' (α : Type u_1) [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (finsetIic : α → Finset α) (mem_Iic : ∀ (a x : α), x ∈ finsetIic a ↔ x ≤ a) : LocallyFiniteOrderBot α

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.

def LocallyFiniteOrderBot.ofIic (α : Type u_1) [PartialOrder α] [DecidableEq α] (finsetIic : α → Finset α) (mem_Iic : ∀ (a x : α), x ∈ finsetIic a ↔ x ≤ a) : LocallyFiniteOrderBot α

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.

@[reducible, inline]

abbrev IsEmpty.toLocallyFiniteOrder {α : Type u_1} [Preorder α] [IsEmpty α] : LocallyFiniteOrder α

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.

@[reducible, inline]

abbrev IsEmpty.toLocallyFiniteOrderTop {α : Type u_1} [Preorder α] [IsEmpty α] : LocallyFiniteOrderTop α

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 : α) => isEmptyElim a, finsetIci := fun (a : α) => isEmptyElim a, finset_mem_Ici := ⋯, finset_mem_Ioi := ⋯ }

@[reducible, inline]

abbrev IsEmpty.toLocallyFiniteOrderBot {α : Type u_1} [Preorder α] [IsEmpty α] : LocallyFiniteOrderBot α

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 : α) => isEmptyElim a, finsetIic := fun (a : α) => isEmptyElim a, finset_mem_Iic := ⋯, finset_mem_Iio := ⋯ }

Intervals as finsets

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

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

Equations

• Finset.Icc a b = LocallyFiniteOrder.finsetIcc a b

def Finset.Ico {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Finset α

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

Equations

• Finset.Ico a b = LocallyFiniteOrder.finsetIco a b

def Finset.Ioc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Finset α

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

Equations

• Finset.Ioc a b = LocallyFiniteOrder.finsetIoc a b

def Finset.Ioo {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Finset α

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

Equations

• Finset.Ioo a b = LocallyFiniteOrder.finsetIoo a b

@[simp]

theorem Finset.mem_Icc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a b x : α} : x ∈ Finset.Icc a b ↔ a ≤ x ∧ x ≤ b

@[simp]

theorem Finset.mem_Ico {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a b x : α} : x ∈ Finset.Ico a b ↔ a ≤ x ∧ x < b

@[simp]

theorem Finset.mem_Ioc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a b x : α} : x ∈ Finset.Ioc a b ↔ a < x ∧ x ≤ b

@[simp]

theorem Finset.mem_Ioo {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a b x : α} : x ∈ Finset.Ioo a b ↔ a < x ∧ x < b

@[simp]

theorem Finset.coe_Icc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : ↑(Finset.Icc a b) = Set.Icc a b

@[simp]

theorem Finset.coe_Ico {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : ↑(Finset.Ico a b) = Set.Ico a b

@[simp]

theorem Finset.coe_Ioc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : ↑(Finset.Ioc a b) = Set.Ioc a b

@[simp]

theorem Finset.coe_Ioo {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : ↑(Finset.Ioo a b) = Set.Ioo a b

def Finset.Ici {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : Finset α

The finset $[a, ∞)$ of elements x such that a ≤ x. Basically Set.Ici a as a finset.

Equations

• Finset.Ici a = LocallyFiniteOrderTop.finsetIci a

def Finset.Ioi {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : Finset α

The finset $(a, ∞)$ of elements x such that a < x. Basically Set.Ioi a as a finset.

Equations

• Finset.Ioi a = LocallyFiniteOrderTop.finsetIoi a

@[simp]

theorem Finset.mem_Ici {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] {a x : α} : x ∈ Finset.Ici a ↔ a ≤ x

@[simp]

theorem Finset.mem_Ioi {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] {a x : α} : x ∈ Finset.Ioi a ↔ a < x

@[simp]

theorem Finset.coe_Ici {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : ↑(Finset.Ici a) = Set.Ici a

@[simp]

theorem Finset.coe_Ioi {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : ↑(Finset.Ioi a) = Set.Ioi a

def Finset.Iic {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (b : α) : Finset α

The finset $(-∞, b]$ of elements x such that x ≤ b. Basically Set.Iic b as a finset.

Equations

• Finset.Iic b = LocallyFiniteOrderBot.finsetIic b

def Finset.Iio {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (b : α) : Finset α

The finset $(-∞, b)$ of elements x such that x < b. Basically Set.Iio b as a finset.

Equations

• Finset.Iio b = LocallyFiniteOrderBot.finsetIio b

@[simp]

theorem Finset.mem_Iic {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] {a x : α} : x ∈ Finset.Iic a ↔ x ≤ a

@[simp]

theorem Finset.mem_Iio {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] {a x : α} : x ∈ Finset.Iio a ↔ x < a

@[simp]

theorem Finset.coe_Iic {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) : ↑(Finset.Iic a) = Set.Iic a

@[simp]

theorem Finset.coe_Iio {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) : ↑(Finset.Iio a) = Set.Iio a

@[instance 100]

instance LocallyFiniteOrder.toLocallyFiniteOrderTop {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] [OrderTop α] : LocallyFiniteOrderTop α

Equations

• LocallyFiniteOrder.toLocallyFiniteOrderTop = { finsetIoi := fun (b : α) => Finset.Ioc b ⊤, finsetIci := fun (b : α) => Finset.Icc b ⊤, finset_mem_Ici := ⋯, finset_mem_Ioi := ⋯ }

theorem Finset.Ici_eq_Icc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] [OrderTop α] (a : α) : Finset.Ici a = Finset.Icc a ⊤

theorem Finset.Ioi_eq_Ioc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] [OrderTop α] (a : α) : Finset.Ioi a = Finset.Ioc a ⊤

@[instance 100]

instance Finset.LocallyFiniteOrder.toLocallyFiniteOrderBot {α : Type u_1} [Preorder α] [OrderBot α] [LocallyFiniteOrder α] : LocallyFiniteOrderBot α

Equations

• Finset.LocallyFiniteOrder.toLocallyFiniteOrderBot = { finsetIio := Finset.Ico ⊥, finsetIic := Finset.Icc ⊥, finset_mem_Iic := ⋯, finset_mem_Iio := ⋯ }

theorem Finset.Iic_eq_Icc {α : Type u_1} [Preorder α] [OrderBot α] [LocallyFiniteOrder α] : Finset.Iic = Finset.Icc ⊥

theorem Finset.Iio_eq_Ico {α : Type u_1} [Preorder α] [OrderBot α] [LocallyFiniteOrder α] : Finset.Iio = Finset.Ico ⊥

def Finset.uIcc {α : Type u_1} [Lattice α] [LocallyFiniteOrder α] (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

• Finset.uIcc a b = Finset.Icc (a ⊓ b) (a ⊔ b)

def FinsetInterval.«term[[_,_]]» : Lean.ParserDescr

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.

@[simp]

theorem Finset.mem_uIcc {α : Type u_1} [Lattice α] [LocallyFiniteOrder α] {a b x : α} : x ∈ Finset.uIcc a b ↔ a ⊓ b ≤ x ∧ x ≤ a ⊔ b

@[simp]

theorem Finset.coe_uIcc {α : Type u_1} [Lattice α] [LocallyFiniteOrder α] (a b : α) : ↑(Finset.uIcc a b) = Set.uIcc a b

def Mathlib.Meta.elabFinsetBuilderIxx : Lean.Elab.Term.TermElab

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 ?α.

See also

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

Finiteness of Set intervals

instance Set.fintypeIcc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Fintype ↑(Set.Icc a b)

Equations

• Set.fintypeIcc a b = Fintype.ofFinset (Finset.Icc a b) ⋯

instance Set.fintypeIco {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Fintype ↑(Set.Ico a b)

Equations

• Set.fintypeIco a b = Fintype.ofFinset (Finset.Ico a b) ⋯

instance Set.fintypeIoc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Fintype ↑(Set.Ioc a b)

Equations

• Set.fintypeIoc a b = Fintype.ofFinset (Finset.Ioc a b) ⋯

instance Set.fintypeIoo {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Fintype ↑(Set.Ioo a b)

Equations

• Set.fintypeIoo a b = Fintype.ofFinset (Finset.Ioo a b) ⋯

theorem Set.finite_Icc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : (Set.Icc a b).Finite

theorem Set.finite_Ico {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : (Set.Ico a b).Finite

theorem Set.finite_Ioc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : (Set.Ioc a b).Finite

theorem Set.finite_Ioo {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : (Set.Ioo a b).Finite

instance Set.fintypeIci {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : Fintype ↑(Set.Ici a)

Equations

• Set.fintypeIci a = Fintype.ofFinset (Finset.Ici a) ⋯

instance Set.fintypeIoi {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : Fintype ↑(Set.Ioi a)

Equations

• Set.fintypeIoi a = Fintype.ofFinset (Finset.Ioi a) ⋯

theorem Set.finite_Ici {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : (Set.Ici a).Finite

theorem Set.finite_Ioi {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : (Set.Ioi a).Finite

instance Set.fintypeIic {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (b : α) : Fintype ↑(Set.Iic b)

Equations

• Set.fintypeIic b = Fintype.ofFinset (Finset.Iic b) ⋯

instance Set.fintypeIio {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (b : α) : Fintype ↑(Set.Iio b)

Equations

• Set.fintypeIio b = Fintype.ofFinset (Finset.Iio b) ⋯

theorem Set.finite_Iic {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (b : α) : (Set.Iic b).Finite

theorem Set.finite_Iio {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (b : α) : (Set.Iio b).Finite

instance Set.fintypeUIcc {α : Type u_1} [Lattice α] [LocallyFiniteOrder α] (a b : α) : Fintype ↑(Set.uIcc a b)

Equations

• Set.fintypeUIcc a b = Fintype.ofFinset (Finset.uIcc a b) ⋯

@[simp]

theorem Set.finite_interval {α : Type u_1} [Lattice α] [LocallyFiniteOrder α] (a b : α) : (Set.uIcc a b).Finite

Instances

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

A noncomputable constructor from the finiteness of all closed intervals.

Equations

• LocallyFiniteOrder.ofFiniteIcc h = LocallyFiniteOrder.ofIcc' α (fun (a b : α) => ⋯.toFinset) ⋯

@[reducible, inline]

abbrev Fintype.toLocallyFiniteOrder {α : Type u_1} [Preorder α] [Fintype α] [DecidableRel fun (x1 x2 : α) => x1 < x2] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : LocallyFiniteOrder α

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.

instance instSubsingletonLocallyFiniteOrder {α : Type u_1} [Preorder α] : Subsingleton (LocallyFiniteOrder α)

Equations

• ⋯ = ⋯

instance instSubsingletonLocallyFiniteOrderTop {α : Type u_1} [Preorder α] : Subsingleton (LocallyFiniteOrderTop α)

Equations

• ⋯ = ⋯

instance instSubsingletonLocallyFiniteOrderBot {α : Type u_1} [Preorder α] : Subsingleton (LocallyFiniteOrderBot α)

Equations

• ⋯ = ⋯

noncomputable def OrderEmbedding.locallyFiniteOrder {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder β] (f : α ↪o β) : LocallyFiniteOrder α

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

Equations

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

OrderDual

instance OrderDual.instLocallyFiniteOrder {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] : LocallyFiniteOrder αᵒᵈ

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_orderDual_def {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : αᵒᵈ) : Finset.Icc a b = Finset.map OrderDual.toDual.toEmbedding (Finset.Icc (OrderDual.ofDual b) (OrderDual.ofDual a))

theorem Finset.Ico_orderDual_def {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : αᵒᵈ) : Finset.Ico a b = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioc (OrderDual.ofDual b) (OrderDual.ofDual a))

theorem Finset.Ioc_orderDual_def {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : αᵒᵈ) : Finset.Ioc a b = Finset.map OrderDual.toDual.toEmbedding (Finset.Ico (OrderDual.ofDual b) (OrderDual.ofDual a))

theorem Finset.Ioo_orderDual_def {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : αᵒᵈ) : Finset.Ioo a b = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioo (OrderDual.ofDual b) (OrderDual.ofDual a))

theorem Finset.Icc_toDual {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (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} [Preorder α] [LocallyFiniteOrder α] (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} [Preorder α] [LocallyFiniteOrder α] (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} [Preorder α] [LocallyFiniteOrder α] (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} [Preorder α] [LocallyFiniteOrder α] (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} [Preorder α] [LocallyFiniteOrder α] (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} [Preorder α] [LocallyFiniteOrder α] (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} [Preorder α] [LocallyFiniteOrder α] (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} [Preorder α] [LocallyFiniteOrderTop α] : LocallyFiniteOrderBot αᵒᵈ

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_orderDual_def {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : αᵒᵈ) : Finset.Iic a = Finset.map OrderDual.toDual.toEmbedding (Finset.Ici (OrderDual.ofDual a))

theorem Iio_orderDual_def {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : αᵒᵈ) : Finset.Iio a = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioi (OrderDual.ofDual a))

theorem Finset.Iic_toDual {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : Finset.Iic (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ici a)

theorem Finset.Iio_toDual {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : Finset.Iio (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioi a)

theorem Finset.Ici_ofDual {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : αᵒᵈ) : Finset.Ici (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Iic a)

theorem Finset.Ioi_ofDual {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : αᵒᵈ) : Finset.Ioi (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Iio a)

instance OrderDual.instLocallyFiniteOrderTop {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] : LocallyFiniteOrderTop αᵒᵈ

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_orderDual_def {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : αᵒᵈ) : Finset.Ici a = Finset.map OrderDual.toDual.toEmbedding (Finset.Iic (OrderDual.ofDual a))

theorem Ioi_orderDual_def {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : αᵒᵈ) : Finset.Ioi a = Finset.map OrderDual.toDual.toEmbedding (Finset.Iio (OrderDual.ofDual a))

theorem Finset.Ici_toDual {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) : Finset.Ici (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Iic a)

theorem Finset.Ioi_toDual {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) : Finset.Ioi (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Iio a)

theorem Finset.Iic_ofDual {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : αᵒᵈ) : Finset.Iic (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ici a)

theorem Finset.Iio_ofDual {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : αᵒᵈ) : Finset.Iio (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ioi a)

Prod

instance Prod.instLocallyFiniteOrder {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableRel fun (x1 x2 : α × β) => x1 ≤ x2] : LocallyFiniteOrder (α × β)

Equations

• Prod.instLocallyFiniteOrder = LocallyFiniteOrder.ofIcc' (α × β) (fun (x y : α × β) => Finset.Icc x.1 y.1 ×ˢ Finset.Icc x.2 y.2) ⋯

theorem Finset.Icc_prod_def {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableRel fun (x1 x2 : α × β) => x1 ≤ x2] (x y : α × β) : Finset.Icc 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} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [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} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [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} [Preorder α] [Preorder β] [LocallyFiniteOrderTop α] [LocallyFiniteOrderTop β] [DecidableRel fun (x1 x2 : α × β) => x1 ≤ x2] : LocallyFiniteOrderTop (α × β)

Equations

• Prod.instLocallyFiniteOrderTop = LocallyFiniteOrderTop.ofIci' (α × β) (fun (x : α × β) => Finset.Ici x.1 ×ˢ Finset.Ici x.2) ⋯

theorem Finset.Ici_prod_def {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrderTop α] [LocallyFiniteOrderTop β] [DecidableRel fun (x1 x2 : α × β) => x1 ≤ x2] (x : α × β) : Finset.Ici x = Finset.Ici x.1 ×ˢ Finset.Ici x.2

theorem Finset.Ici_product_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrderTop α] [LocallyFiniteOrderTop β] [DecidableRel fun (x1 x2 : α × β) => x1 ≤ x2] (a : α) (b : β) : Finset.Ici a ×ˢ Finset.Ici b = Finset.Ici (a, b)

theorem Finset.card_Ici_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrderTop α] [LocallyFiniteOrderTop β] [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} [Preorder α] [Preorder β] [LocallyFiniteOrderBot α] [LocallyFiniteOrderBot β] [DecidableRel fun (x1 x2 : α × β) => x1 ≤ x2] : LocallyFiniteOrderBot (α × β)

Equations

• Prod.instLocallyFiniteOrderBot = LocallyFiniteOrderBot.ofIic' (α × β) (fun (x : α × β) => Finset.Iic x.1 ×ˢ Finset.Iic x.2) ⋯

theorem Finset.Iic_prod_def {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrderBot α] [LocallyFiniteOrderBot β] [DecidableRel fun (x1 x2 : α × β) => x1 ≤ x2] (x : α × β) : Finset.Iic x = Finset.Iic x.1 ×ˢ Finset.Iic x.2

theorem Finset.Iic_product_Iic {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrderBot α] [LocallyFiniteOrderBot β] [DecidableRel fun (x1 x2 : α × β) => x1 ≤ x2] (a : α) (b : β) : Finset.Iic a ×ˢ Finset.Iic b = Finset.Iic (a, b)

theorem Finset.card_Iic_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrderBot α] [LocallyFiniteOrderBot β] [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} [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableRel fun (x1 x2 : α × β) => x1 ≤ x2] (x y : α × β) : Finset.uIcc 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} [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [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} [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [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) [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] : LocallyFiniteOrder (WithTop α)

Equations

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

theorem WithTop.Icc_coe_top (α : Type u_1) [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] (a : α) : Finset.Icc ↑a ⊤ = Finset.insertNone (Finset.Ici a)

theorem WithTop.Icc_coe_coe (α : Type u_1) [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] (a b : α) : Finset.Icc ↑a ↑b = Finset.map Function.Embedding.some (Finset.Icc a b)

theorem WithTop.Ico_coe_top (α : Type u_1) [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] (a : α) : Finset.Ico ↑a ⊤ = Finset.map Function.Embedding.some (Finset.Ici a)

theorem WithTop.Ico_coe_coe (α : Type u_1) [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] (a b : α) : Finset.Ico ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ico a b)

theorem WithTop.Ioc_coe_top (α : Type u_1) [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] (a : α) : Finset.Ioc ↑a ⊤ = Finset.insertNone (Finset.Ioi a)

theorem WithTop.Ioc_coe_coe (α : Type u_1) [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] (a b : α) : Finset.Ioc ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ioc a b)

theorem WithTop.Ioo_coe_top (α : Type u_1) [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] (a : α) : Finset.Ioo ↑a ⊤ = Finset.map Function.Embedding.some (Finset.Ioi a)

theorem WithTop.Ioo_coe_coe (α : Type u_1) [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] (a b : α) : Finset.Ioo ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ioo a b)

instance WithBot.instLocallyFiniteOrder (α : Type u_1) [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] : LocallyFiniteOrder (WithBot α)

Equations

• WithBot.instLocallyFiniteOrder α = OrderDual.instLocallyFiniteOrder

theorem WithBot.Icc_bot_coe (α : Type u_1) [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] (b : α) : Finset.Icc ⊥ ↑b = Finset.insertNone (Finset.Iic b)

theorem WithBot.Icc_coe_coe (α : Type u_1) [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] (a b : α) : Finset.Icc ↑a ↑b = Finset.map Function.Embedding.some (Finset.Icc a b)

theorem WithBot.Ico_bot_coe (α : Type u_1) [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] (b : α) : Finset.Ico ⊥ ↑b = Finset.insertNone (Finset.Iio b)

theorem WithBot.Ico_coe_coe (α : Type u_1) [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] (a b : α) : Finset.Ico ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ico a b)

theorem WithBot.Ioc_bot_coe (α : Type u_1) [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] (b : α) : Finset.Ioc ⊥ ↑b = Finset.map Function.Embedding.some (Finset.Iic b)

theorem WithBot.Ioc_coe_coe (α : Type u_1) [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] (a b : α) : Finset.Ioc ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ioc a b)

theorem WithBot.Ioo_bot_coe (α : Type u_1) [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] (b : α) : Finset.Ioo ⊥ ↑b = Finset.map Function.Embedding.some (Finset.Iio b)

theorem WithBot.Ioo_coe_coe (α : Type u_1) [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] (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} [Preorder α] [Preorder β] [LocallyFiniteOrder β] (f : α ≃o β) : LocallyFiniteOrder α

Transfer LocallyFiniteOrder across an OrderIso.

Equations

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

@[reducible, inline]

abbrev OrderIso.locallyFiniteOrderTop {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrderTop β] (f : α ≃o β) : LocallyFiniteOrderTop α

Transfer LocallyFiniteOrderTop across an OrderIso.

Equations

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

@[reducible, inline]

abbrev OrderIso.locallyFiniteOrderBot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrderBot β] (f : α ≃o β) : LocallyFiniteOrderBot α

Transfer LocallyFiniteOrderBot across an OrderIso.

Equations

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

Subtype of a locally finite order

instance Subtype.instLocallyFiniteOrder {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrder α] : LocallyFiniteOrder (Subtype p)

Equations

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

instance Subtype.instLocallyFiniteOrderTop {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrderTop α] : LocallyFiniteOrderTop (Subtype p)

Equations

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

instance Subtype.instLocallyFiniteOrderBot {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrderBot α] : LocallyFiniteOrderBot (Subtype p)

Equations

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

theorem Finset.subtype_Icc_eq {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrder α] (a b : Subtype p) : Finset.Icc a b = Finset.subtype p (Finset.Icc ↑a ↑b)

theorem Finset.subtype_Ico_eq {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrder α] (a b : Subtype p) : Finset.Ico a b = Finset.subtype p (Finset.Ico ↑a ↑b)

theorem Finset.subtype_Ioc_eq {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrder α] (a b : Subtype p) : Finset.Ioc a b = Finset.subtype p (Finset.Ioc ↑a ↑b)

theorem Finset.subtype_Ioo_eq {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrder α] (a b : Subtype p) : Finset.Ioo a b = Finset.subtype p (Finset.Ioo ↑a ↑b)

theorem Finset.map_subtype_embedding_Icc {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrder α] (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

theorem Finset.map_subtype_embedding_Ico {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrder α] (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

theorem Finset.map_subtype_embedding_Ioc {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrder α] (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

theorem Finset.map_subtype_embedding_Ioo {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrder α] (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

theorem Finset.subtype_Ici_eq {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrderTop α] (a : Subtype p) : Finset.Ici a = Finset.subtype p (Finset.Ici ↑a)

theorem Finset.subtype_Ioi_eq {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrderTop α] (a : Subtype p) : Finset.Ioi a = Finset.subtype p (Finset.Ioi ↑a)

theorem Finset.map_subtype_embedding_Ici {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrderTop α] (a : Subtype p) (hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x) : Finset.map (Function.Embedding.subtype p) (Finset.Ici a) = Finset.Ici ↑a

theorem Finset.map_subtype_embedding_Ioi {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrderTop α] (a : Subtype p) (hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x) : Finset.map (Function.Embedding.subtype p) (Finset.Ioi a) = Finset.Ioi ↑a

theorem Finset.subtype_Iic_eq {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrderBot α] (a : Subtype p) : Finset.Iic a = Finset.subtype p (Finset.Iic ↑a)

theorem Finset.subtype_Iio_eq {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrderBot α] (a : Subtype p) : Finset.Iio a = Finset.subtype p (Finset.Iio ↑a)

theorem Finset.map_subtype_embedding_Iic {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrderBot α] (a : Subtype p) (hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x) : Finset.map (Function.Embedding.subtype p) (Finset.Iic a) = Finset.Iic ↑a

theorem Finset.map_subtype_embedding_Iio {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrderBot α] (a : Subtype p) (hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x) : Finset.map (Function.Embedding.subtype p) (Finset.Iio a) = Finset.Iio ↑a

theorem BddBelow.finite_of_bddAbove {α : Type u_3} [Preorder α] [LocallyFiniteOrder α] {s : Set α} (h₀ : BddBelow s) (h₁ : BddAbove s) : s.Finite

theorem Set.finite_iff_bddAbove {α : Type u_3} {s : Set α} [SemilatticeSup α] [LocallyFiniteOrder α] [OrderBot α] : s.Finite ↔ BddAbove s

theorem Set.finite_iff_bddBelow {α : Type u_3} {s : Set α} [SemilatticeInf α] [LocallyFiniteOrder α] [OrderTop α] : s.Finite ↔ BddBelow s

theorem Set.finite_iff_bddBelow_bddAbove {α : Type u_3} {s : Set α} [Nonempty α] [Lattice α] [LocallyFiniteOrder α] : s.Finite ↔ BddBelow s ∧ BddAbove s

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

@[instance 100]

instance instLocallyFiniteOrderTopSubtypeLeOfDecidableRelOfLocallyFiniteOrder {α : Type u_1} {y : α} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [LocallyFiniteOrder α] : 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 : α} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] [LocallyFiniteOrder α] : 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 : α} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [LocallyFiniteOrder α] : 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 : α} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] [LocallyFiniteOrder α] : LocallyFiniteOrderBot { x : α // y < x }

Equations

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

instance instFiniteSubtypeLeOfLocallyFiniteOrderBot {α : Type u_1} {y : α} [Preorder α] [LocallyFiniteOrderBot α] : Finite { x : α // x ≤ y }

Equations

• ⋯ = ⋯

instance instFiniteSubtypeLtOfLocallyFiniteOrderBot {α : Type u_1} {y : α} [Preorder α] [LocallyFiniteOrderBot α] : Finite { x : α // x < y }

Equations

• ⋯ = ⋯

instance instFiniteSubtypeLeOfLocallyFiniteOrderTop {α : Type u_1} {y : α} [Preorder α] [LocallyFiniteOrderTop α] : Finite { x : α // y ≤ x }

Equations

• ⋯ = ⋯

instance instFiniteSubtypeLtOfLocallyFiniteOrderTop {α : Type u_1} {y : α} [Preorder α] [LocallyFiniteOrderTop α] : Finite { x : α // y < x }

Equations

• ⋯ = ⋯

@[simp]

theorem Set.toFinset_Icc {α : Type u_3} [Preorder α] [LocallyFiniteOrder α] (a b : α) [Fintype ↑(Set.Icc a b)] : (Set.Icc a b).toFinset = Finset.Icc a b

@[simp]

theorem Set.toFinset_Ico {α : Type u_3} [Preorder α] [LocallyFiniteOrder α] (a b : α) [Fintype ↑(Set.Ico a b)] : (Set.Ico a b).toFinset = Finset.Ico a b

@[simp]

theorem Set.toFinset_Ioc {α : Type u_3} [Preorder α] [LocallyFiniteOrder α] (a b : α) [Fintype ↑(Set.Ioc a b)] : (Set.Ioc a b).toFinset = Finset.Ioc a b

@[simp]

theorem Set.toFinset_Ioo {α : Type u_3} [Preorder α] [LocallyFiniteOrder α] (a b : α) [Fintype ↑(Set.Ioo a b)] : (Set.Ioo a b).toFinset = Finset.Ioo a b

@[simp]

theorem Set.toFinset_Ici {α : Type u_3} [Preorder α] [LocallyFiniteOrderTop α] (a : α) [Fintype ↑(Set.Ici a)] : (Set.Ici a).toFinset = Finset.Ici a

@[simp]

theorem Set.toFinset_Ioi {α : Type u_3} [Preorder α] [LocallyFiniteOrderTop α] (a : α) [Fintype ↑(Set.Ioi a)] : (Set.Ioi a).toFinset = Finset.Ioi a

@[simp]

theorem Set.toFinset_Iic {α : Type u_3} [Preorder α] [LocallyFiniteOrderBot α] (a : α) [Fintype ↑(Set.Iic a)] : (Set.Iic a).toFinset = Finset.Iic a

@[simp]

theorem Set.toFinset_Iio {α : Type u_3} [Preorder α] [LocallyFiniteOrderBot α] (a : α) [Fintype ↑(Set.Iio a)] : (Set.Iio a).toFinset = Finset.Iio a

@[reducible, inline]

abbrev LocallyFiniteOrder.ofOrderIsoClass {F : Type u_3} {M : Type u_4} {N : Type u_5} [Preorder M] [Preorder N] [EquivLike F M N] [OrderIsoClass F M N] (f : F) [LocallyFiniteOrder N] : LocallyFiniteOrder M

A LocallyFiniteOrder can be transferred across an order isomorphism.

Equations

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