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 := 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.

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

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

      Instances
        def LocallyFiniteOrder.ofIcc' (α : Type u_1) [Preorder α] [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.
        Instances For
          def LocallyFiniteOrder.ofIcc (α : Type u_1) [PartialOrder α] [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.
          Instances For
            def LocallyFiniteOrderTop.ofIci' (α : Type u_1) [Preorder α] [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.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) [PartialOrder α] [DecidableEq α] (finsetIci : αFinset α) (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) [Preorder α] [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 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) [PartialOrder α] [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 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]

                    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]

                      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 := }
                      Instances For
                        @[reducible]

                        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 := }
                        Instances For

                          Intervals as finsets #

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

                                  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} [Preorder α] [LocallyFiniteOrderTop α] (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} [Preorder α] [LocallyFiniteOrderTop α] {a : α} {x : α} :
                                      @[simp]
                                      theorem Finset.mem_Ioi {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] {a : α} {x : α} :
                                      @[simp]
                                      theorem Finset.coe_Ici {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) :
                                      @[simp]
                                      theorem Finset.coe_Ioi {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) :
                                      def Finset.Iic {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (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} [Preorder α] [LocallyFiniteOrderBot α] (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} [Preorder α] [LocallyFiniteOrderBot α] {a : α} {x : α} :
                                          @[simp]
                                          theorem Finset.mem_Iio {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] {a : α} {x : α} :
                                          @[simp]
                                          theorem Finset.coe_Iic {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) :
                                          @[simp]
                                          theorem Finset.coe_Iio {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) :
                                          Equations
                                          • LocallyFiniteOrder.toLocallyFiniteOrderTop = { finsetIoi := fun (b : α) => Finset.Ioc b , finsetIci := fun (b : α) => Finset.Icc b , finset_mem_Ici := , finset_mem_Ioi := }
                                          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.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} [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

                                              Intervals as multisets #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                                              Finiteness of Set intervals #

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

                                                              Instances #

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

                                                              A noncomputable constructor from the finiteness of all closed intervals.

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

                                                                A fintype is a locally finite order.

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

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  noncomputable def OrderEmbedding.locallyFiniteOrder {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [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.
                                                                  Instances For

                                                                    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} [Preorder α] [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} [Preorder α] [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} [Preorder α] [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} [Preorder α] [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} [Preorder α] [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} [Preorder α] [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} [Preorder α] [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} [Preorder α] [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} [Preorder α] [LocallyFiniteOrderTop α] (a : α) :
                                                                    Finset.Iic (OrderDual.toDual a) = Finset.map (Equiv.toEmbedding OrderDual.toDual) (Finset.Ici a)
                                                                    theorem Iio_toDual {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) :
                                                                    Finset.Iio (OrderDual.toDual a) = Finset.map (Equiv.toEmbedding OrderDual.toDual) (Finset.Ioi a)
                                                                    theorem Ici_ofDual {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : αᵒᵈ) :
                                                                    Finset.Ici (OrderDual.ofDual a) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) (Finset.Iic a)
                                                                    theorem Ioi_ofDual {α : Type u_1} [Preorder α] [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} [Preorder α] [LocallyFiniteOrderBot α] (a : α) :
                                                                    Finset.Ici (OrderDual.toDual a) = Finset.map (Equiv.toEmbedding OrderDual.toDual) (Finset.Iic a)
                                                                    theorem Ioi_toDual {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) :
                                                                    Finset.Ioi (OrderDual.toDual a) = Finset.map (Equiv.toEmbedding OrderDual.toDual) (Finset.Iio a)
                                                                    theorem Iic_ofDual {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : αᵒᵈ) :
                                                                    Finset.Iic (OrderDual.ofDual a) = Finset.map (Equiv.toEmbedding OrderDual.ofDual) (Finset.Ici a)
                                                                    theorem Iio_ofDual {α : Type u_1} [Preorder α] [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} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableRel fun (x x_1 : α × β) => x x_1] :
                                                                    Equations
                                                                    Equations
                                                                    Equations
                                                                    theorem Prod.Icc_eq {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableRel fun (x x_1 : α × β) => x x_1] (p : α × β) (q : α × β) :
                                                                    Finset.Icc p q = Finset.Icc p.1 q.1 ×ˢ Finset.Icc p.2 q.2
                                                                    @[simp]
                                                                    theorem Prod.Icc_mk_mk {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [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} [Preorder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableRel fun (x x_1 : α × β) => x x_1] (p : α × β) (q : α × β) :
                                                                    (Finset.Icc p q).card = (Finset.Icc p.1 q.1).card * (Finset.Icc p.2 q.2).card
                                                                    theorem Prod.uIcc_eq {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableRel fun (x x_1 : α × β) => x x_1] (p : α × β) (q : α × β) :
                                                                    @[simp]
                                                                    theorem Prod.uIcc_mk_mk {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [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} [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableRel fun (x x_1 : α × β) => x x_1] (p : α × β) (q : α × β) :
                                                                    (Finset.uIcc p q).card = (Finset.uIcc p.1 q.1).card * (Finset.uIcc p.2 q.2).card

                                                                    WithTop, WithBot #

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

                                                                    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)
                                                                    Equations
                                                                    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]
                                                                    def OrderIso.locallyFiniteOrder {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [LocallyFiniteOrder β] (f : α ≃o β) :

                                                                    Transfer LocallyFiniteOrder across an OrderIso.

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

                                                                      Transfer LocallyFiniteOrderTop across an OrderIso.

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

                                                                        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 #

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          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 : Subtype p) (b : Subtype p) :
                                                                          theorem Finset.subtype_Ico_eq {α : Type u_1} [Preorder α] (p : αProp) [DecidablePred p] [LocallyFiniteOrder α] (a : Subtype p) (b : Subtype p) :
                                                                          theorem Finset.subtype_Ioc_eq {α : Type u_1} [Preorder α] (p : αProp) [DecidablePred p] [LocallyFiniteOrder α] (a : Subtype p) (b : Subtype p) :
                                                                          theorem Finset.subtype_Ioo_eq {α : Type u_1} [Preorder α] (p : αProp) [DecidablePred p] [LocallyFiniteOrder α] (a : Subtype p) (b : Subtype p) :
                                                                          theorem Finset.map_subtype_embedding_Icc {α : Type u_1} [Preorder α] (p : αProp) [DecidablePred p] [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} [Preorder α] (p : αProp) [DecidablePred p] [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} [Preorder α] (p : αProp) [DecidablePred p] [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} [Preorder α] (p : αProp) [DecidablePred p] [LocallyFiniteOrder α] (a : Subtype p) (b : Subtype p) (hp : ∀ ⦃a b x : α⦄, a xx bp ap bp x) :
                                                                          theorem Finset.map_subtype_embedding_Ici {α : Type u_1} [Preorder α] (p : αProp) [DecidablePred p] [LocallyFiniteOrderTop α] (a : Subtype p) (hp : ∀ ⦃a x : α⦄, a xp ap x) :
                                                                          theorem Finset.map_subtype_embedding_Ioi {α : Type u_1} [Preorder α] (p : αProp) [DecidablePred p] [LocallyFiniteOrderTop α] (a : Subtype p) (hp : ∀ ⦃a x : α⦄, a xp ap x) :
                                                                          theorem Finset.map_subtype_embedding_Iic {α : Type u_1} [Preorder α] (p : αProp) [DecidablePred p] [LocallyFiniteOrderBot α] (a : Subtype p) (hp : ∀ ⦃a x : α⦄, x ap ap x) :
                                                                          theorem Finset.map_subtype_embedding_Iio {α : Type u_1} [Preorder α] (p : αProp) [DecidablePred p] [LocallyFiniteOrderBot α] (a : Subtype p) (hp : ∀ ⦃a x : α⦄, x ap ap x) :
                                                                          theorem BddBelow.finite_of_bddAbove {α : Type u_3} [Preorder α] [LocallyFiniteOrder α] {s : Set α} (h₀ : BddBelow s) (h₁ : BddAbove s) :

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

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