Documentation

Mathlib.Order.Fin.Basic

Fin n forms a bounded linear order #

This file contains the linear ordered instance on Fin n.

Fin n is the type whose elements are natural numbers smaller than n. This file expands on the development in the core library.

Main definitions #

Instances #

Equations
Equations
  • Fin.instBoundedOrder = BoundedOrder.mk

Extra instances to short-circuit type class resolution #

These also prevent non-computable instances being used to construct these instances non-computably.

Equations
  • Fin.instPartialOrder = inferInstance
instance Fin.instLattice {n : } :
Equations
  • Fin.instLattice = inferInstance

Miscellaneous lemmas #

theorem Fin.bot_eq_zero (n : ) :
= 0
@[simp]
theorem Fin.rev_bot {n : } [NeZero n] :
.rev =
@[simp]
theorem Fin.rev_top {n : } [NeZero n] :
.rev =
theorem Fin.rev_last_eq_bot (n : ) :
(Fin.last n).rev =
theorem Fin.strictMono_pred_comp {n : } {α : Type u_1} [Preorder α] {f : αFin (n + 1)} (hf : ∀ (a : α), f a 0) (hf₂ : StrictMono f) :
StrictMono fun (a : α) => (f a).pred
theorem Fin.monotone_pred_comp {n : } {α : Type u_1} [Preorder α] {f : αFin (n + 1)} (hf : ∀ (a : α), f a 0) (hf₂ : Monotone f) :
Monotone fun (a : α) => (f a).pred
theorem Fin.strictMono_castPred_comp {n : } {α : Type u_1} [Preorder α] {f : αFin (n + 1)} (hf : ∀ (a : α), f a Fin.last n) (hf₂ : StrictMono f) :
StrictMono fun (a : α) => (f a).castPred
theorem Fin.monotone_castPred_comp {n : } {α : Type u_1} [Preorder α] {f : αFin (n + 1)} (hf : ∀ (a : α), f a Fin.last n) (hf₂ : Monotone f) :
Monotone fun (a : α) => (f a).castPred
theorem Fin.strictMono_iff_lt_succ {n : } {α : Type u_1} [Preorder α] {f : Fin (n + 1)α} :
StrictMono f ∀ (i : Fin n), f i.castSucc < f i.succ

A function f on Fin (n + 1) is strictly monotone if and only if f i < f (i + 1) for all i.

theorem Fin.monotone_iff_le_succ {n : } {α : Type u_1} [Preorder α] {f : Fin (n + 1)α} :
Monotone f ∀ (i : Fin n), f i.castSucc f i.succ

A function f on Fin (n + 1) is monotone if and only if f i ≤ f (i + 1) for all i.

theorem Fin.strictAnti_iff_succ_lt {n : } {α : Type u_1} [Preorder α] {f : Fin (n + 1)α} :
StrictAnti f ∀ (i : Fin n), f i.succ < f i.castSucc

A function f on Fin (n + 1) is strictly antitone if and only if f (i + 1) < f i for all i.

theorem Fin.antitone_iff_succ_le {n : } {α : Type u_1} [Preorder α] {f : Fin (n + 1)α} :
Antitone f ∀ (i : Fin n), f i.succ f i.castSucc

A function f on Fin (n + 1) is antitone if and only if f (i + 1) ≤ f i for all i.

Monotonicity #

theorem Fin.val_strictMono {n : } :
StrictMono Fin.val
theorem Fin.strictMono_succ {n : } :
StrictMono Fin.succ
theorem Fin.strictMono_castLE {m : } {n : } (h : n m) :
theorem Fin.strictMono_castSucc {n : } :
StrictMono Fin.castSucc
theorem Fin.strictMono_addNat {n : } (m : ) :
StrictMono fun (x : Fin n) => x.addNat m
theorem Fin.strictMono_succAbove {n : } (p : Fin (n + 1)) :
StrictMono p.succAbove
theorem Fin.succAbove_lt_succAbove_iff {n : } {p : Fin (n + 1)} {i : Fin n} {j : Fin n} :
p.succAbove i < p.succAbove j i < j
theorem Fin.succAbove_le_succAbove_iff {n : } {p : Fin (n + 1)} {i : Fin n} {j : Fin n} :
p.succAbove i p.succAbove j i j
theorem Fin.predAbove_right_monotone {n : } (p : Fin n) :
Monotone p.predAbove
theorem Fin.predAbove_left_monotone {n : } (i : Fin (n + 1)) :
Monotone fun (p : Fin n) => p.predAbove i
@[simp]
theorem Fin.predAboveOrderHom_coe {n : } (p : Fin n) (i : Fin (n + 1)) :
p.predAboveOrderHom i = p.predAbove i
def Fin.predAboveOrderHom {n : } (p : Fin n) :
Fin (n + 1) →o Fin n

Fin.predAbove p as an OrderHom.

Equations
  • p.predAboveOrderHom = { toFun := p.predAbove, monotone' := }
Instances For

    Order isomorphisms #

    @[simp]
    theorem Fin.orderIsoSubtype_symm_apply {n : } (a : { i : // i < n }) :
    (RelIso.symm Fin.orderIsoSubtype) a = a,
    @[simp]
    theorem Fin.orderIsoSubtype_apply {n : } (a : Fin n) :
    Fin.orderIsoSubtype a = a,
    def Fin.orderIsoSubtype {n : } :
    Fin n ≃o { i : // i < n }

    The equivalence Fin n ≃ {i // i < n} is an order isomorphism.

    Equations
    • Fin.orderIsoSubtype = Fin.equivSubtype.toOrderIso
    Instances For
      @[simp]
      theorem Fin.castOrderIso_symm_apply {m : } {n : } (eq : n = m) (i : Fin m) :
      @[simp]
      theorem Fin.castOrderIso_apply {m : } {n : } (eq : n = m) (i : Fin n) :
      def Fin.castOrderIso {m : } {n : } (eq : n = m) :

      Fin.cast as an OrderIso.

      castOrderIso eq i embeds i into an equal Fin type.

      Equations
      Instances For
        @[deprecated Fin.castOrderIso]
        def Fin.castIso {m : } {n : } (eq : n = m) :

        Alias of Fin.castOrderIso.


        Fin.cast as an OrderIso.

        castOrderIso eq i embeds i into an equal Fin type.

        Equations
        Instances For
          @[simp]
          theorem Fin.symm_castOrderIso {m : } {n : } (h : n = m) :
          @[deprecated Fin.symm_castOrderIso]
          theorem Fin.symm_castIso {m : } {n : } (h : n = m) :

          Alias of Fin.symm_castOrderIso.

          @[simp]
          theorem Fin.castOrderIso_refl {n : } (h : optParam (n = n) ) :
          @[deprecated Fin.castOrderIso_refl]
          theorem Fin.castIso_refl {n : } (h : optParam (n = n) ) :

          Alias of Fin.castOrderIso_refl.

          theorem Fin.castOrderIso_toEquiv {m : } {n : } (h : n = m) :
          (Fin.castOrderIso h).toEquiv = Equiv.cast

          While in many cases Fin.castOrderIso is better than Equiv.cast/cast, sometimes we want to apply a generic lemma about cast.

          @[deprecated Fin.castOrderIso_toEquiv]
          theorem Fin.castIso_to_equiv {m : } {n : } (h : n = m) :
          (Fin.castOrderIso h).toEquiv = Equiv.cast

          Alias of Fin.castOrderIso_toEquiv.


          While in many cases Fin.castOrderIso is better than Equiv.cast/cast, sometimes we want to apply a generic lemma about cast.

          @[simp]
          theorem Fin.revOrderIso_apply {n : } :
          ∀ (a : (Fin n)ᵒᵈ), Fin.revOrderIso a = (OrderDual.ofDual a).rev
          @[simp]
          theorem Fin.revOrderIso_toEquiv {n : } :
          Fin.revOrderIso.toEquiv = OrderDual.ofDual.trans Fin.revPerm

          Fin.rev n as an order-reversing isomorphism.

          Equations
          • Fin.revOrderIso = { toEquiv := OrderDual.ofDual.trans Fin.revPerm, map_rel_iff' := }
          Instances For
            @[simp]
            theorem Fin.revOrderIso_symm_apply {n : } (i : Fin n) :
            Fin.revOrderIso.symm i = OrderDual.toDual i.rev

            Order embeddings #

            @[simp]
            theorem Fin.valOrderEmb_apply (n : ) (self : Fin n) :
            (Fin.valOrderEmb n) self = self

            The inclusion map Fin n → ℕ is an order embedding.

            Equations
            Instances For
              instance Fin.Lt.isWellOrder (n : ) :
              IsWellOrder (Fin n) fun (x1 x2 : Fin n) => x1 < x2

              The ordering on Fin n is a well order.

              Equations
              • =
              def Fin.succOrderEmb (n : ) :
              Fin n ↪o Fin (n + 1)

              Fin.succ as an OrderEmbedding

              Equations
              Instances For
                @[simp]
                theorem Fin.coe_succOrderEmb {n : } :
                (Fin.succOrderEmb n) = Fin.succ
                @[simp]
                theorem Fin.castLEOrderEmb_apply {m : } {n : } (h : n m) (i : Fin n) :
                @[simp]
                theorem Fin.castLEOrderEmb_toEmbedding {m : } {n : } (h : n m) :
                (Fin.castLEOrderEmb h).toEmbedding = { toFun := Fin.castLE h, inj' := }
                def Fin.castLEOrderEmb {m : } {n : } (h : n m) :

                Fin.castLE as an OrderEmbedding.

                castLEEmb h i embeds i into a larger Fin type.

                Equations
                Instances For
                  @[simp]
                  theorem Fin.castAddOrderEmb_toEmbedding {n : } (m : ) :
                  (Fin.castAddOrderEmb m).toEmbedding = { toFun := Fin.castAdd m, inj' := }
                  @[simp]
                  theorem Fin.castAddOrderEmb_apply {n : } (m : ) :
                  ∀ (a : Fin n), (Fin.castAddOrderEmb m) a = Fin.castAdd m a
                  def Fin.castAddOrderEmb {n : } (m : ) :
                  Fin n ↪o Fin (n + m)

                  Fin.castAdd as an OrderEmbedding.

                  castAddEmb m i embeds i : Fin n in Fin (n+m). See also Fin.natAddEmb and Fin.addNatEmb.

                  Equations
                  Instances For
                    @[simp]
                    theorem Fin.castSuccOrderEmb_toEmbedding {n : } :
                    Fin.castSuccOrderEmb.toEmbedding = { toFun := Fin.castSucc, inj' := }
                    @[simp]
                    theorem Fin.castSuccOrderEmb_apply {n : } :
                    ∀ (a : Fin n), Fin.castSuccOrderEmb a = a.castSucc
                    def Fin.castSuccOrderEmb {n : } :
                    Fin n ↪o Fin (n + 1)

                    Fin.castSucc as an OrderEmbedding.

                    castSuccOrderEmb i embeds i : Fin n in Fin (n+1).

                    Equations
                    Instances For
                      @[simp]
                      theorem Fin.addNatOrderEmb_apply {n : } (m : ) :
                      ∀ (x : Fin n), (Fin.addNatOrderEmb m) x = x.addNat m
                      @[simp]
                      theorem Fin.addNatOrderEmb_toEmbedding {n : } (m : ) :
                      (Fin.addNatOrderEmb m).toEmbedding = { toFun := fun (x : Fin n) => x.addNat m, inj' := }
                      def Fin.addNatOrderEmb {n : } (m : ) :
                      Fin n ↪o Fin (n + m)

                      Fin.addNat as an OrderEmbedding.

                      addNatOrderEmb m i adds m to i, generalizes Fin.succ.

                      Equations
                      Instances For
                        @[simp]
                        theorem Fin.natAddOrderEmb_toEmbedding {m : } (n : ) :
                        (Fin.natAddOrderEmb n).toEmbedding = { toFun := Fin.natAdd n, inj' := }
                        @[simp]
                        theorem Fin.natAddOrderEmb_apply {m : } (n : ) (i : Fin m) :
                        def Fin.natAddOrderEmb {m : } (n : ) :
                        Fin m ↪o Fin (n + m)

                        Fin.natAdd as an OrderEmbedding.

                        natAddOrderEmb n i adds n to i "on the left".

                        Equations
                        Instances For
                          @[simp]
                          theorem Fin.succAboveOrderEmb_apply {n : } (p : Fin (n + 1)) (i : Fin n) :
                          p.succAboveOrderEmb i = p.succAbove i
                          @[simp]
                          theorem Fin.succAboveOrderEmb_toEmbedding {n : } (p : Fin (n + 1)) :
                          p.succAboveOrderEmb.toEmbedding = { toFun := p.succAbove, inj' := }
                          def Fin.succAboveOrderEmb {n : } (p : Fin (n + 1)) :
                          Fin n ↪o Fin (n + 1)

                          Fin.succAbove p as an OrderEmbedding.

                          Equations
                          Instances For

                            Uniqueness of order isomorphisms #

                            @[simp]
                            theorem Fin.coe_orderIso_apply {m : } {n : } (e : Fin n ≃o Fin m) (i : Fin n) :
                            (e i) = i

                            If e is an orderIso between Fin n and Fin m, then n = m and e is the identity map. In this lemma we state that for each i : Fin n we have (e i : ℕ) = (i : ℕ).

                            instance Fin.orderIso_subsingleton {n : } {α : Type u_1} [Preorder α] :
                            Equations
                            • =
                            instance Fin.orderIso_subsingleton' {n : } {α : Type u_1} [Preorder α] :
                            Equations
                            • =
                            instance Fin.orderIsoUnique {n : } :
                            Equations
                            theorem Fin.strictMono_unique {n : } {α : Type u_1} [Preorder α] {f : Fin nα} {g : Fin nα} (hf : StrictMono f) (hg : StrictMono g) (h : Set.range f = Set.range g) :
                            f = g

                            Two strictly monotone functions from Fin n are equal provided that their ranges are equal.

                            theorem Fin.orderEmbedding_eq {n : } {α : Type u_1} [Preorder α] {f : Fin n ↪o α} {g : Fin n ↪o α} (h : Set.range f = Set.range g) :
                            f = g

                            Two order embeddings of Fin n are equal provided that their ranges are equal.