Documentation

Mathlib.Order.Fin.Tuple

Order properties on tuples #

theorem Fin.pi_lex_lt_cons_cons {n : } {α : Fin (n + 1)Type u_1} {x₀ : α 0} {y₀ : α 0} {x : (i : Fin n) → α i.succ} {y : (i : Fin n) → α i.succ} (s : {i : Fin n.succ} → α iα iProp) :
Pi.Lex (fun (x1 x2 : Fin n.succ) => x1 < x2) s (Fin.cons x₀ x) (Fin.cons y₀ y) s x₀ y₀ x₀ = y₀ Pi.Lex (fun (x1 x2 : Fin n) => x1 < x2) (fun (i : Fin n) => s) x y
theorem Fin.insertNth_mem_Icc {n : } {α : Fin (n + 1)Type u_1} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (i.succAbove j)} {q₁ : (j : Fin (n + 1)) → α j} {q₂ : (j : Fin (n + 1)) → α j} :
i.insertNth x p Set.Icc q₁ q₂ x Set.Icc (q₁ i) (q₂ i) p Set.Icc (fun (j : Fin n) => q₁ (i.succAbove j)) fun (j : Fin n) => q₂ (i.succAbove j)
theorem Fin.preimage_insertNth_Icc_of_mem {n : } {α : Fin (n + 1)Type u_1} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {q₁ : (j : Fin (n + 1)) → α j} {q₂ : (j : Fin (n + 1)) → α j} (hx : x Set.Icc (q₁ i) (q₂ i)) :
i.insertNth x ⁻¹' Set.Icc q₁ q₂ = Set.Icc (fun (j : Fin n) => q₁ (i.succAbove j)) fun (j : Fin n) => q₂ (i.succAbove j)
theorem Fin.preimage_insertNth_Icc_of_not_mem {n : } {α : Fin (n + 1)Type u_1} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {q₁ : (j : Fin (n + 1)) → α j} {q₂ : (j : Fin (n + 1)) → α j} (hx : xSet.Icc (q₁ i) (q₂ i)) :
i.insertNth x ⁻¹' Set.Icc q₁ q₂ =
theorem liftFun_vecCons {α : Type u_1} {n : } (r : ααProp) [IsTrans α r] {f : Fin (n + 1)α} {a : α} :
((fun (x1 x2 : Fin (n + 1).succ) => x1 < x2) r) (Matrix.vecCons a f) (Matrix.vecCons a f) r a (f 0) ((fun (x1 x2 : Fin (n + 1)) => x1 < x2) r) f f
@[simp]
theorem strictMono_vecCons {α : Type u_1} [Preorder α] {n : } {f : Fin (n + 1)α} {a : α} :
@[simp]
theorem monotone_vecCons {α : Type u_1} [Preorder α] {n : } {f : Fin (n + 1)α} {a : α} :
@[simp]
theorem monotone_vecEmpty {α : Type u_1} [Preorder α] {a : α} :
@[simp]
theorem strictMono_vecEmpty {α : Type u_1} [Preorder α] {a : α} :
@[simp]
theorem strictAnti_vecCons {α : Type u_1} [Preorder α] {n : } {f : Fin (n + 1)α} {a : α} :
@[simp]
theorem antitone_vecCons {α : Type u_1} [Preorder α] {n : } {f : Fin (n + 1)α} {a : α} :
@[simp]
theorem antitone_vecEmpty {α : Type u_1} [Preorder α] {a : α} :
@[simp]
theorem strictAnti_vecEmpty {α : Type u_1} [Preorder α] {a : α} :
theorem StrictMono.vecCons {α : Type u_1} [Preorder α] {n : } {f : Fin (n + 1)α} {a : α} (hf : StrictMono f) (ha : a < f 0) :
theorem StrictAnti.vecCons {α : Type u_1} [Preorder α] {n : } {f : Fin (n + 1)α} {a : α} (hf : StrictAnti f) (ha : f 0 < a) :
theorem Monotone.vecCons {α : Type u_1} [Preorder α] {n : } {f : Fin (n + 1)α} {a : α} (hf : Monotone f) (ha : a f 0) :
theorem Antitone.vecCons {α : Type u_1} [Preorder α] {n : } {f : Fin (n + 1)α} {a : α} (hf : Antitone f) (ha : f 0 a) :
def OrderIso.piFinTwoIso (α : Fin 2Type u_2) [(i : Fin 2) → Preorder (α i)] :
((i : Fin 2) → α i) ≃o α 0 × α 1

Π i : Fin 2, α i is order equivalent to α 0 × α 1. See also OrderIso.finTwoArrowEquiv for a non-dependent version.

Equations
Instances For
    def OrderIso.finTwoArrowIso (α : Type u_2) [Preorder α] :
    (Fin 2α) ≃o α × α

    The space of functions Fin 2 → α is order equivalent to α × α. See also OrderIso.piFinTwoIso.

    Equations
    Instances For
      @[simp]
      theorem Fin.consOrderIso_apply {n : } (α : Fin (n + 1)Type u_2) [(i : Fin (n + 1)) → LE (α i)] (f : α 0 × ((i : Fin n) → α i.succ)) (i : Fin (n + 1)) :
      (Fin.consOrderIso α) f i = Fin.cons f.1 f.2 i
      @[simp]
      theorem Fin.consOrderIso_symm_apply {n : } (α : Fin (n + 1)Type u_2) [(i : Fin (n + 1)) → LE (α i)] (f : (i : Fin (n + 1)) → α i) :
      @[simp]
      theorem Fin.consOrderIso_toEquiv {n : } (α : Fin (n + 1)Type u_2) [(i : Fin (n + 1)) → LE (α i)] :
      def Fin.consOrderIso {n : } (α : Fin (n + 1)Type u_2) [(i : Fin (n + 1)) → LE (α i)] :
      α 0 × ((i : Fin n) → α i.succ) ≃o ((i : Fin (n + 1)) → α i)

      Order isomorphism between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the first element of the tuple.

      This is Fin.cons as an OrderIso.

      Equations
      Instances For
        @[simp]
        theorem Fin.snocOrderIso_symm_apply {n : } (α : Fin (n + 1)Type u_2) [(i : Fin (n + 1)) → LE (α i)] (f : (i : Fin (n + 1)) → α i) :
        @[simp]
        theorem Fin.snocOrderIso_apply {n : } (α : Fin (n + 1)Type u_2) [(i : Fin (n + 1)) → LE (α i)] (f : α (Fin.last n) × ((i : Fin n) → α i.castSucc)) :
        ∀ (x : Fin (n + 1)), (Fin.snocOrderIso α) f x = Fin.snoc f.2 f.1 x
        @[simp]
        theorem Fin.snocOrderIso_toEquiv {n : } (α : Fin (n + 1)Type u_2) [(i : Fin (n + 1)) → LE (α i)] :
        def Fin.snocOrderIso {n : } (α : Fin (n + 1)Type u_2) [(i : Fin (n + 1)) → LE (α i)] :
        α (Fin.last n) × ((i : Fin n) → α i.castSucc) ≃o ((i : Fin (n + 1)) → α i)

        Order isomorphism between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the last element of the tuple.

        This is Fin.snoc as an OrderIso.

        Equations
        Instances For
          @[simp]
          theorem Fin.insertNthOrderIso_symm_apply {n : } (α : Fin (n + 1)Type u_2) [(i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1)) (f : (i : Fin (n + 1)) → α i) :
          (RelIso.symm (Fin.insertNthOrderIso α p)) f = (f p, p.removeNth f)
          @[simp]
          theorem Fin.insertNthOrderIso_apply {n : } (α : Fin (n + 1)Type u_2) [(i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1)) (f : α p × ((i : Fin n) → α (p.succAbove i))) (j : Fin (n + 1)) :
          (Fin.insertNthOrderIso α p) f j = p.insertNth f.1 f.2 j
          @[simp]
          theorem Fin.insertNthOrderIso_toEquiv {n : } (α : Fin (n + 1)Type u_2) [(i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1)) :
          def Fin.insertNthOrderIso {n : } (α : Fin (n + 1)Type u_2) [(i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1)) :
          α p × ((i : Fin n) → α (p.succAbove i)) ≃o ((i : Fin (n + 1)) → α i)

          Order isomorphism between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the p-th element of the tuple.

          This is Fin.insertNth as an OrderIso.

          Equations
          Instances For
            @[simp]
            theorem Fin.insertNthOrderIso_zero {n : } (α : Fin (n + 1)Type u_2) [(i : Fin (n + 1)) → LE (α i)] :
            @[simp]
            theorem Fin.insertNthOrderIso_last (n : ) (α : Type u_2) [LE α] :
            Fin.insertNthOrderIso (fun (x : Fin (n + 1)) => α) (Fin.last n) = Fin.snocOrderIso fun (x : Fin (n + 1)) => α

            Note this lemma can only be written about non-dependent tuples as insertNth (last n) = snoc is not a definitional equality.

            @[deprecated Fin.insertNthOrderIso]
            def OrderIso.piFinSuccAboveIso {n : } (α : Fin (n + 1)Type u_2) [(i : Fin (n + 1)) → LE (α i)] (i : Fin (n + 1)) :
            ((j : Fin (n + 1)) → α j) ≃o α i × ((j : Fin n) → α (i.succAbove j))

            Order isomorphism between Π j : Fin (n + 1), α j and α i × Π j : Fin n, α (Fin.succAbove i j).

            Equations
            Instances For
              def finSuccAboveOrderIso {n : } (p : Fin (n + 1)) :
              Fin n ≃o { x : Fin (n + 1) // x p }

              Fin.succAbove as an order isomorphism between Fin n and {x : Fin (n + 1) // x ≠ p}.

              Equations
              Instances For
                theorem finSuccAboveOrderIso_apply {n : } (p : Fin (n + 1)) (i : Fin n) :
                (finSuccAboveOrderIso p) i = p.succAbove i,
                theorem finSuccAboveOrderIso_symm_apply_last {n : } (x : { x : Fin (n + 1) // x Fin.last n }) :
                (finSuccAboveOrderIso (Fin.last n)).symm x = (↑x).castLT
                theorem finSuccAboveOrderIso_symm_apply_ne_last {n : } {p : Fin (n + 1)} (h : p Fin.last n) (x : { x : Fin (n + 1) // x p }) :
                (finSuccAboveEquiv p).symm x = (p.castLT ).predAbove x
                @[simp]
                theorem Fin.castLEOrderIso_apply {n : } {m : } (h : n m) (i : Fin n) :
                (Fin.castLEOrderIso h) i = Fin.castLE h i,
                @[simp]
                theorem Fin.castLEOrderIso_symm_apply {n : } {m : } (h : n m) (i : { i : Fin m // i < n }) :
                (RelIso.symm (Fin.castLEOrderIso h)) i = i,
                def Fin.castLEOrderIso {n : } {m : } (h : n m) :
                Fin n ≃o { i : Fin m // i < n }

                Promote a Fin n into a larger Fin m, as a subtype where the underlying values are retained. This is the OrderIso version of Fin.castLE.

                Equations
                • Fin.castLEOrderIso h = { toFun := fun (i : Fin n) => Fin.castLE h i, , invFun := fun (i : { i : Fin m // i < n }) => i, , left_inv := , right_inv := , map_rel_iff' := }
                Instances For