# Nonempty finite linear orders
Nonempty finite linear orders form the index category for simplicial objects.
@[instance]
@[instance]
@[instance]
@[instance]
@[class]
- elems : finset α
- complete : ∀ (x : α), x ∈ nonempty_fin_lin_ord.elems
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
- decidable_le : decidable_rel has_le.le
- decidable_eq : decidable_eq α
- decidable_lt : decidable_rel has_lt.lt
- bot : α
- bot_le : ∀ (a : α), ⊥ ≤ a
- top : α
- le_top : ∀ (a : α), a ≤ ⊤
A typeclass for nonempty finite linear orders.
@[instance]
Equations
- punit.nonempty_fin_lin_ord = {elems := fintype.elems punit punit.fintype, complete := _, le := decidable_linear_ordered_cancel_add_comm_monoid.le punit.decidable_linear_ordered_cancel_add_comm_monoid, lt := decidable_linear_ordered_cancel_add_comm_monoid.lt punit.decidable_linear_ordered_cancel_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := decidable_linear_ordered_cancel_add_comm_monoid.decidable_le punit.decidable_linear_ordered_cancel_add_comm_monoid, decidable_eq := decidable_linear_ordered_cancel_add_comm_monoid.decidable_eq punit.decidable_linear_ordered_cancel_add_comm_monoid, decidable_lt := decidable_linear_ordered_cancel_add_comm_monoid.decidable_lt punit.decidable_linear_ordered_cancel_add_comm_monoid, bot := punit.star, bot_le := punit.nonempty_fin_lin_ord._proof_1, top := punit.star, le_top := punit.nonempty_fin_lin_ord._proof_2}
@[instance]
Equations
- fin.nonempty_fin_lin_ord n = {elems := fintype.elems (fin (n + 1)) (fin.fintype (n + 1)), complete := _, le := decidable_linear_order.le fin.decidable_linear_order, lt := decidable_linear_order.lt fin.decidable_linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := decidable_linear_order.decidable_le fin.decidable_linear_order, decidable_eq := decidable_linear_order.decidable_eq fin.decidable_linear_order, decidable_lt := decidable_linear_order.decidable_lt fin.decidable_linear_order, bot := 0, bot_le := _, top := fin.last n, le_top := _}
@[instance]
Equations
- ulift.nonempty_fin_lin_ord α = {elems := fintype.elems (ulift α) (ulift.fintype α), complete := _, le := linear_order.le (linear_order.lift ⇑equiv.ulift _), lt := linear_order.lt (linear_order.lift ⇑equiv.ulift _), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (_x : ulift α), ulift.nonempty_fin_lin_ord._match_4 α _x, decidable_eq := decidable_linear_order.decidable_eq._default linear_order.le linear_order.lt _ _ _ _ _ (λ (_x : ulift α), ulift.nonempty_fin_lin_ord._match_4 α _x), decidable_lt := decidable_linear_order.decidable_lt._default linear_order.le linear_order.lt _ _ _ _ _ (λ (_x : ulift α), ulift.nonempty_fin_lin_ord._match_4 α _x), bot := {down := ⊥}, bot_le := _, top := {down := ⊤}, le_top := _}
- ulift.nonempty_fin_lin_ord._match_4 α {down := a} = λ (_x : ulift α), ulift.nonempty_fin_lin_ord._match_3 α a _x
- ulift.nonempty_fin_lin_ord._match_3 α a {down := b} = decidable_linear_order.decidable_le (⇑equiv.ulift {down := a}) (⇑equiv.ulift {down := b})
The category of nonempty finite linear orders.
@[instance]
Construct a bundled NonemptyFinLinOrd from the underlying type and typeclass.
Equations
@[instance]
@[instance]
Equations
- α.nonempty_fin_lin_ord = α.str