Documentation

Mathlib.Order.LocallyFinite

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,

In a LocallyFiniteOrderTop,

In a LocallyFiniteOrderBot,

Instances #

A LocallyFiniteOrder instance can be built

Instances for concrete types are proved in their respective files:

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 :=
begin -- very non golfed
  have h : (Finset.Ioc x ub).Nonempty := ⟨ub, Finset.mem_Ioc_iff.2 ⟨hx, le_rfl⟩⟩
  use Finset.min' (Finset.Ioc x ub) h
  constructor
  · have := Finset.min'_mem _ h
    simp * at *
  rintro y hxy
  obtain hy | hy := le_total y ub
  apply Finset.min'_le
  simp * at *
  exact (Finset.min'_le _ _ (Finset.mem_Ioc_iff.2 ⟨hx, le_rfl⟩)).trans hy
end

Note that the converse is not true. Consider {-2^z | z : ℤ} ∪ {2^z | z : ℤ}. Any element has a successor (and actually a predecessor as well), so it is a SuccOrder, but it's not locally finite as Icc (-1) 1 is infinite.

class LocallyFiniteOrder (α : Type u_1) [inst : Preorder α] :
Type u_1
  • Left-closed right-closed interval

    finsetIcc : ααFinset α
  • Left-closed right-open interval

    finsetIco : ααFinset α
  • Left-open right-closed interval

    finsetIoc : ααFinset α
  • Left-open right-open interval

    finsetIoo : ααFinset α
  • x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b

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

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

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

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

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

Instances
    class LocallyFiniteOrderTop (α : Type u_1) [inst : Preorder α] :
    Type u_1
    • Left-open right-infinite interval

      finsetIoi : αFinset α
    • Left-closed right-infinite interval

      finsetIci : αFinset α
    • x ∈ finsetIci a ↔ a ≤ x

      finset_mem_Ici : ∀ (a x : α), x finsetIci a a x
    • x ∈ finsetIoi a ↔ a < x

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

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

    Instances
      class LocallyFiniteOrderBot (α : Type u_1) [inst : Preorder α] :
      Type u_1
      • Left-infinite right-open interval

        finsetIio : αFinset α
      • Left-infinite right-closed interval

        finsetIic : αFinset α
      • x ∈ finsetIic a ↔ x ≤ a

        finset_mem_Iic : ∀ (a x : α), x finsetIic a x a
      • x ∈ finsetIio a ↔ x < a

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

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

      Instances
        def LocallyFiniteOrder.ofIcc' (α : Type u_1) [inst : Preorder α] [inst : DecidableRel fun x x_1 => x x_1] (finsetIcc : ααFinset α) (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.
        def LocallyFiniteOrder.ofIcc (α : Type u_1) [inst : PartialOrder α] [inst : DecidableEq α] (finsetIcc : ααFinset α) (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.
        def LocallyFiniteOrderTop.ofIci' (α : Type u_1) [inst : Preorder α] [inst : DecidableRel fun x x_1 => x x_1] (finsetIci : αFinset α) (mem_Ici : ∀ (a x : α), x finsetIci a a x) :

        A constructor from a definition of Finset.Iic 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) [inst : PartialOrder α] [inst : DecidableEq α] (finsetIci : αFinset α) (mem_Ici : ∀ (a x : α), x finsetIci a a x) :

        A constructor from a definition of Finset.Iic 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) [inst : Preorder α] [inst : DecidableRel fun x x_1 => x x_1] (finsetIic : αFinset α) (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 LocallyFiniteOrder.ofIcc, this one requires DecidableRel (· ≤ ·) but only Preorder.

        Equations
        • One or more equations did not get rendered due to their size.
        def LocallyFiniteOrderTop.ofIic (α : Type u_1) [inst : PartialOrder α] [inst : DecidableEq α] (finsetIic : αFinset α) (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 LocallyFiniteOrderTop.ofIci', this one requires PartialOrder but only DecidableEq.

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

        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.

        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.

        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.

        Intervals as finsets #

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

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

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

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

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

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

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

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

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

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

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

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

        Equations
        @[simp]
        theorem Finset.mem_Ici {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] {a : α} {x : α} :
        @[simp]
        theorem Finset.mem_Ioi {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] {a : α} {x : α} :
        @[simp]
        theorem Finset.coe_Ici {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] (a : α) :
        @[simp]
        theorem Finset.coe_Ioi {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] (a : α) :
        def Finset.Iic {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] (a : α) :

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

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

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

        Equations
        @[simp]
        theorem Finset.mem_Iic {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] {a : α} {x : α} :
        @[simp]
        theorem Finset.mem_Iio {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] {a : α} {x : α} :
        @[simp]
        theorem Finset.coe_Iic {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] (a : α) :
        @[simp]
        theorem Finset.coe_Iio {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] (a : α) :
        Equations
        • One or more equations did not get rendered due to their size.
        theorem Finset.Ici_eq_Icc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] [inst : OrderTop α] (a : α) :
        theorem Finset.Ioi_eq_Ioc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] [inst : OrderTop α] (a : α) :
        Equations
        • One or more equations did not get rendered due to their size.
        theorem Finset.Iic_eq_Icc {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] [inst : LocallyFiniteOrder α] :
        Finset.Iic = Finset.Icc
        theorem Finset.Iio_eq_Ico {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] [inst : LocallyFiniteOrder α] :
        Finset.Iio = Finset.Ico
        def Finset.uIcc {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] (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

        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} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {x : α} :
        x Finset.uIcc a b a b x x a b
        @[simp]
        theorem Finset.coe_uIcc {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        ↑(Finset.uIcc a b) = Set.uIcc a b

        Intervals as multisets #

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

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

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

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

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

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

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

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

        Equations
        @[simp]
        theorem Multiset.mem_Icc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {x : α} :
        x Multiset.Icc a b a x x b
        @[simp]
        theorem Multiset.mem_Ico {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {x : α} :
        x Multiset.Ico a b a x x < b
        @[simp]
        theorem Multiset.mem_Ioc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {x : α} :
        x Multiset.Ioc a b a < x x b
        @[simp]
        theorem Multiset.mem_Ioo {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {x : α} :
        x Multiset.Ioo a b a < x x < b
        def Multiset.Ici {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] (a : α) :

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

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

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

        Equations
        @[simp]
        theorem Multiset.mem_Ici {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] {a : α} {x : α} :
        @[simp]
        theorem Multiset.mem_Ioi {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] {a : α} {x : α} :
        def Multiset.Iic {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] (b : α) :

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

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

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

        Equations
        @[simp]
        theorem Multiset.mem_Iic {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] {b : α} {x : α} :
        @[simp]
        theorem Multiset.mem_Iio {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] {b : α} {x : α} :

        Finiteness of Set intervals #

        instance Set.fintypeIcc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Fintype ↑(Set.Icc a b)
        Equations
        instance Set.fintypeIco {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Fintype ↑(Set.Ico a b)
        Equations
        instance Set.fintypeIoc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Fintype ↑(Set.Ioc a b)
        Equations
        instance Set.fintypeIoo {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Fintype ↑(Set.Ioo a b)
        Equations
        theorem Set.finite_Icc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        theorem Set.finite_Ico {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        theorem Set.finite_Ioc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        theorem Set.finite_Ioo {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        instance Set.fintypeIci {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] (a : α) :
        Equations
        instance Set.fintypeIoi {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] (a : α) :
        Equations
        theorem Set.finite_Ici {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] (a : α) :
        theorem Set.finite_Ioi {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] (a : α) :
        instance Set.fintypeIic {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] (b : α) :
        Equations
        instance Set.fintypeIio {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] (b : α) :
        Equations
        theorem Set.finite_Iic {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] (b : α) :
        theorem Set.finite_Iio {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] (b : α) :

        Instances #

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

        A noncomputable constructor from the finiteness of all closed intervals.

        Equations
        def Fintype.toLocallyFiniteOrder {α : Type u_1} [inst : Preorder α] [inst : Fintype α] [inst : DecidableRel fun x x_1 => x < x_1] [inst : 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.
        noncomputable def OrderEmbedding.locallyFiniteOrder {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : LocallyFiniteOrder β] (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.

        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} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Finset.Icc (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map (Equiv.toEmbedding OrderDual.toDual) (Finset.Icc b a)
        theorem Ico_toDual {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Finset.Ico (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map (Equiv.toEmbedding OrderDual.toDual) (Finset.Ioc b a)
        theorem Ioc_toDual {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Finset.Ioc (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map (Equiv.toEmbedding OrderDual.toDual) (Finset.Ico b a)
        theorem Ioo_toDual {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Finset.Ioo (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map (Equiv.toEmbedding OrderDual.toDual) (Finset.Ioo b a)
        theorem Icc_ofDual {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : αᵒᵈ) (b : αᵒᵈ) :
        Finset.Icc (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) (Finset.Icc b a)
        theorem Ico_ofDual {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : αᵒᵈ) (b : αᵒᵈ) :
        Finset.Ico (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) (Finset.Ioc b a)
        theorem Ioc_ofDual {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : αᵒᵈ) (b : αᵒᵈ) :
        Finset.Ioc (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) (Finset.Ico b a)
        theorem Ioo_ofDual {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : αᵒᵈ) (b : αᵒᵈ) :
        Finset.Ioo (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) (Finset.Ioo b a)

        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} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] (a : α) :
        Finset.Iic (OrderDual.toDual a) = Finset.map (Equiv.toEmbedding OrderDual.toDual) (Finset.Ici a)
        theorem Iio_toDual {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] (a : α) :
        Finset.Iio (OrderDual.toDual a) = Finset.map (Equiv.toEmbedding OrderDual.toDual) (Finset.Ioi a)
        theorem Ici_ofDual {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] (a : αᵒᵈ) :
        Finset.Ici (OrderDual.ofDual a) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) (Finset.Iic a)
        theorem Ioi_ofDual {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] (a : αᵒᵈ) :
        Finset.Ioi (OrderDual.ofDual a) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) (Finset.Iio a)

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

        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) [inst : PartialOrder α] [inst : OrderTop α] [inst : LocallyFiniteOrder α] :
        Equations
        • One or more equations did not get rendered due to their size.
        theorem WithTop.Icc_coe_top (α : Type u_1) [inst : PartialOrder α] [inst : OrderTop α] [inst : LocallyFiniteOrder α] (a : α) :
        Finset.Icc a = Finset.insertNone.toEmbedding (Finset.Ici a)
        theorem WithTop.Icc_coe_coe (α : Type u_1) [inst : PartialOrder α] [inst : OrderTop α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Finset.Icc a b = Finset.map Function.Embedding.some (Finset.Icc a b)
        theorem WithTop.Ico_coe_top (α : Type u_1) [inst : PartialOrder α] [inst : OrderTop α] [inst : LocallyFiniteOrder α] (a : α) :
        Finset.Ico a = Finset.map Function.Embedding.some (Finset.Ici a)
        theorem WithTop.Ico_coe_coe (α : Type u_1) [inst : PartialOrder α] [inst : OrderTop α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Finset.Ico a b = Finset.map Function.Embedding.some (Finset.Ico a b)
        theorem WithTop.Ioc_coe_top (α : Type u_1) [inst : PartialOrder α] [inst : OrderTop α] [inst : LocallyFiniteOrder α] (a : α) :
        Finset.Ioc a = Finset.insertNone.toEmbedding (Finset.Ioi a)
        theorem WithTop.Ioc_coe_coe (α : Type u_1) [inst : PartialOrder α] [inst : OrderTop α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Finset.Ioc a b = Finset.map Function.Embedding.some (Finset.Ioc a b)
        theorem WithTop.Ioo_coe_top (α : Type u_1) [inst : PartialOrder α] [inst : OrderTop α] [inst : LocallyFiniteOrder α] (a : α) :
        Finset.Ioo a = Finset.map Function.Embedding.some (Finset.Ioi a)
        theorem WithTop.Ioo_coe_coe (α : Type u_1) [inst : PartialOrder α] [inst : OrderTop α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Finset.Ioo a b = Finset.map Function.Embedding.some (Finset.Ioo a b)
        theorem WithBot.Icc_bot_coe (α : Type u_1) [inst : PartialOrder α] [inst : OrderBot α] [inst : LocallyFiniteOrder α] (b : α) :
        Finset.Icc b = Finset.insertNone.toEmbedding (Finset.Iic b)
        theorem WithBot.Icc_coe_coe (α : Type u_1) [inst : PartialOrder α] [inst : OrderBot α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Finset.Icc a b = Finset.map Function.Embedding.some (Finset.Icc a b)
        theorem WithBot.Ico_bot_coe (α : Type u_1) [inst : PartialOrder α] [inst : OrderBot α] [inst : LocallyFiniteOrder α] (b : α) :
        Finset.Ico b = Finset.insertNone.toEmbedding (Finset.Iio b)
        theorem WithBot.Ico_coe_coe (α : Type u_1) [inst : PartialOrder α] [inst : OrderBot α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Finset.Ico a b = Finset.map Function.Embedding.some (Finset.Ico a b)
        theorem WithBot.Ioc_bot_coe (α : Type u_1) [inst : PartialOrder α] [inst : OrderBot α] [inst : LocallyFiniteOrder α] (b : α) :
        Finset.Ioc b = Finset.map Function.Embedding.some (Finset.Iic b)
        theorem WithBot.Ioc_coe_coe (α : Type u_1) [inst : PartialOrder α] [inst : OrderBot α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Finset.Ioc a b = Finset.map Function.Embedding.some (Finset.Ioc a b)
        theorem WithBot.Ioo_bot_coe (α : Type u_1) [inst : PartialOrder α] [inst : OrderBot α] [inst : LocallyFiniteOrder α] (b : α) :
        Finset.Ioo b = Finset.map Function.Embedding.some (Finset.Iio b)
        theorem WithBot.Ioo_coe_coe (α : Type u_1) [inst : PartialOrder α] [inst : OrderBot α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
        Finset.Ioo a b = Finset.map Function.Embedding.some (Finset.Ioo a b)

        Transfer locally finite orders across order isomorphisms #

        def OrderIso.locallyFiniteOrder {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : LocallyFiniteOrder β] (f : α ≃o β) :

        Transfer LocallyFiniteOrder across an OrderIso.

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

        Transfer LocallyFiniteOrderTop across an OrderIso.

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

        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 instLocallyFiniteOrderSubtypePreorder {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrder α] :
        Equations
        • One or more equations did not get rendered due to their size.
        instance instLocallyFiniteOrderTopSubtypePreorder {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrderTop α] :
        Equations
        • One or more equations did not get rendered due to their size.
        instance instLocallyFiniteOrderBotSubtypePreorder {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrderBot α] :
        Equations
        • One or more equations did not get rendered due to their size.
        theorem Finset.subtype_Icc_eq {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrder α] (a : Subtype p) (b : Subtype p) :
        theorem Finset.subtype_Ico_eq {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrder α] (a : Subtype p) (b : Subtype p) :
        theorem Finset.subtype_Ioc_eq {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrder α] (a : Subtype p) (b : Subtype p) :
        theorem Finset.subtype_Ioo_eq {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrder α] (a : Subtype p) (b : Subtype p) :
        theorem Finset.map_subtype_embedding_Icc {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrder α] (a : Subtype p) (b : Subtype p) (hp : a b x : α⦄ → a xx bp ap bp x) :
        theorem Finset.map_subtype_embedding_Ico {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrder α] (a : Subtype p) (b : Subtype p) (hp : a b x : α⦄ → a xx bp ap bp x) :
        theorem Finset.map_subtype_embedding_Ioc {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrder α] (a : Subtype p) (b : Subtype p) (hp : a b x : α⦄ → a xx bp ap bp x) :
        theorem Finset.map_subtype_embedding_Ioo {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrder α] (a : Subtype p) (b : Subtype p) (hp : a b x : α⦄ → a xx bp ap bp x) :
        theorem Finset.subtype_Ici_eq {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrderTop α] (a : Subtype p) :
        theorem Finset.subtype_Ioi_eq {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrderTop α] (a : Subtype p) :
        theorem Finset.map_subtype_embedding_Ici {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrderTop α] (a : Subtype p) (hp : a x : α⦄ → a xp ap x) :
        theorem Finset.map_subtype_embedding_Ioi {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrderTop α] (a : Subtype p) (hp : a x : α⦄ → a xp ap x) :
        theorem Finset.subtype_Iic_eq {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrderBot α] (a : Subtype p) :
        theorem Finset.subtype_Iio_eq {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrderBot α] (a : Subtype p) :
        theorem Finset.map_subtype_embedding_Iic {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrderBot α] (a : Subtype p) (hp : a x : α⦄ → x ap ap x) :
        theorem Finset.map_subtype_embedding_Iio {α : Type u_1} [inst : Preorder α] (p : αProp) [inst : DecidablePred p] [inst : LocallyFiniteOrderBot α] (a : Subtype p) (hp : a x : α⦄ → x ap ap x) :