Documentation

Mathlib.Order.Category.NonemptyFinLinOrd

Nonempty finite linear orders #

This defines NonemptyFinLinOrd, the category of nonempty finite linear orders with monotone maps. This is the index category for simplicial objects.

Note: NonemptyFinLinOrd is not a subcategory of FinBddDistLat because its morphisms do not preserve and .

class NonemptyFiniteLinearOrder (α : Type u_1) extends Fintype , LinearOrder :
Type u_1

A typeclass for nonempty finite linear orders.

  • elems : Finset α
  • complete : ∀ (x : α), x Fintype.elems
  • le : ααProp
  • lt : ααProp
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • min : ααα
  • max : ααα
  • compare : ααOrdering
  • le_total : ∀ (a b : α), a b b a
  • decidableLE : DecidableRel fun (x1 x2 : α) => x1 x2
  • decidableEq : DecidableEq α
  • decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
  • min_def : ∀ (a b : α), min a b = if a b then a else b
  • max_def : ∀ (a b : α), max a b = if a b then b else a
  • compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
  • Nonempty : Nonempty α
Instances
    def NonemptyFinLinOrd :
    Type (u_1 + 1)

    The category of nonempty finite linear orders.

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

      Construct a bundled NonemptyFinLinOrd from the underlying type and typeclass.

      Equations
      Instances For
        Equations
        • α.instNonemptyFiniteLinearOrderα = α.str
        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.
        @[simp]
        @[simp]
        theorem NonemptyFinLinOrd.Iso.mk_inv {α : NonemptyFinLinOrd} {β : NonemptyFinLinOrd} (e : α ≃o β) :
        (NonemptyFinLinOrd.Iso.mk e).inv = e.symm
        def NonemptyFinLinOrd.Iso.mk {α : NonemptyFinLinOrd} {β : NonemptyFinLinOrd} (e : α ≃o β) :
        α β

        Constructs an equivalence between nonempty finite linear orders from an order isomorphism between them.

        Equations
        Instances For
          @[simp]
          theorem NonemptyFinLinOrd.dual_map :
          ∀ {X Y : NonemptyFinLinOrd} (a : X →o Y), NonemptyFinLinOrd.dual.map a = OrderHom.dual a

          OrderDual as a functor.

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

            The equivalence between NonemptyFinLinOrd and itself induced by OrderDual both ways.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • NonemptyFinLinOrd.instFunLikeHomαNonemptyFiniteLinearOrder = { coe := fun (f : A B) => (let_fun this := f; this), coe_injective' := }

              The forgetful functor NonemptyFinLinOrdFinPartOrd and OrderDual commute.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def Fin.hom_succ {n : } (i : Fin n) :
                i.castSucc i.succ

                The generating arrow i ⟶ i+1 in the category Fin n.

                Equations
                Instances For