Skip to main content

Module functions

oxilean_std::ordering

Module functions 

Source
Expand description

Auto-generated module

πŸ€– Generated with SplitRS

Functions§

axiom_antichain_maximal_ty
Type of Antichain.maximal: a maximal antichain in a partial order. Antichain.maximal : PartialOrder β†’ Type
axiom_bounded_lattice_ty
Type of BoundedLattice: a lattice with top and bottom elements. BoundedLattice : Type β†’ Type 1
axiom_cantor_back_and_forth_ty
Type of Cantor.backAndForth: any two countable dense linear orders without endpoints are isomorphic. Cantor.backAndForth : Prop
axiom_cofinal_subset_ty
Type of CofinalSubset: a subset S of a poset is cofinal if every element has an upper bound in S. CofinalSubset : βˆ€ {P : Type} [PartialOrder P], (P β†’ Prop) β†’ Prop
axiom_cofinality_ordinal_ty
Type of Cofinality.ordinal: the cofinality of an ordinal. Cofinality.ordinal : Ordinal β†’ Ordinal
axiom_complete_lattice_sup_ty
Type of CompleteLattice.sup: supremum of an arbitrary set. CompleteLattice.sup : βˆ€ {L : Type} [CompleteLattice L], (L β†’ Prop) β†’ L
axiom_dedekind_completeness_ty
Type of DedekindCut.completeness: every Dedekind cut has a supremum. DedekindCut.completeness : βˆ€ F : Type, DedekindCut F β†’ F
axiom_dedekind_cut_ty
Type of DedekindCut: a Dedekind cut in an ordered field. DedekindCut : Type β†’ Type
axiom_dense_linear_order_ty
Type of DenseLinearOrder: a dense linear order without endpoints. DenseLinearOrder : Type β†’ Prop
axiom_dickson_lemma_ty
Type of Dickson.lemma: the product of WQOs is a WQO. Dickson.lemma : WQO β†’ WQO β†’ WQO
axiom_dickson_nat_wqo_ty
Type of Dickson.nat_wqo: (Nat, ≀) is a WQO. Dickson.nat_wqo : WQO
axiom_dilworth_theorem_ty
Type of Dilworth.theorem: in any finite partial order, the minimum number of chains needed to cover all elements equals the maximum antichain size. Dilworth.theorem : PartialOrder β†’ Prop
axiom_fraisse_limit_ty
Type of Fraisse.limit: the FraΓ―ssΓ© limit of a class of finite structures. Fraisse.limit : StructureClass β†’ Structure
axiom_galois_connection_ty
Type of GaloisConnection: a Galois connection between two posets. GaloisConnection : βˆ€ (P Q : Type) [PartialOrder P] [PartialOrder Q], (P β†’ Q) β†’ (Q β†’ P) β†’ Prop
axiom_hausdorff_scattered_ty
Type of Hausdorff.scatteredOrder: a scattered linear order embeds no dense suborder. Hausdorff.scatteredOrder : Type β†’ Prop
axiom_hausdorff_theorem_ty
Type of Hausdorff.theorem: every linear order decomposes into a scattered and a dense part. Hausdorff.theorem : LinearOrder β†’ Prop
axiom_higman_lemma_ty
Type of Higman.lemma: finite words over a WQO form a WQO under embedding. Higman.lemma : WQO β†’ WQO
axiom_kruskal_tree_thm_ty
Type of Kruskal.treeThm: finite rooted trees over a WQO form a WQO under topological embedding. Kruskal.treeThm : WQO β†’ WQO
axiom_linear_order_ty
Type of LinearOrder: a type equipped with a total order. LinearOrder : Type β†’ Type 1
axiom_mirsky_theorem_ty
Type of Mirsky.theorem: the minimum number of antichains covering a partial order equals the length of the longest chain. Mirsky.theorem : PartialOrder β†’ Prop
axiom_order_embedding_ty
Type of OrderEmbedding: an order embedding (injective order homomorphism). OrderEmbedding : Type β†’ Type β†’ Type 1
axiom_order_iso_ty
Type of OrderIso: an order isomorphism between two ordered sets. OrderIso : Type β†’ Type β†’ Type 1
axiom_ordered_field_archimedean_ty
Type of OrderedField.archimedean: an ordered field is Archimedean if for every x > 0, there exists n : Nat with n > x. OrderedField.archimedean : βˆ€ F, OrderedField F β†’ Prop
axiom_ordered_field_ty
Type of OrderedField: a field with a compatible total order. OrderedField : Type β†’ Prop
axiom_ordinal_add_ty
Type of Ordinal.add: ordinal addition. Ordinal.add : Ordinal β†’ Ordinal β†’ Ordinal
axiom_ordinal_church_kleene_ty
Type of Ordinal.churchKleene: the Church-Kleene ordinal ω₁^CK. Ordinal.churchKleene : Ordinal
axiom_ordinal_cnf_ty
Type of Ordinal.cnfNF: Cantor Normal Form of an ordinal. Ordinal.cnfNF : Ordinal β†’ List (Ordinal Γ— Nat)
axiom_ordinal_comparability_ty
Type of Ordinal.comparability: any two ordinals are comparable. Ordinal.comparability : βˆ€ Ξ± Ξ² : Ordinal, Ξ± < Ξ² ∨ Ξ± = Ξ² ∨ Ξ² < Ξ±
axiom_ordinal_epsilon0_ty
Type of Ordinal.epsilon0: the ordinal Ξ΅β‚€ = sup{Ο‰, Ο‰^Ο‰, Ο‰^(Ο‰^Ο‰), …}. Ordinal.epsilon0 : Ordinal
axiom_ordinal_is_limit_ty
Type of Ordinal.isLimit: predicate for limit ordinals. Ordinal.isLimit : Ordinal β†’ Prop
axiom_ordinal_le_ty
Type of Ordinal.le: weak ordering on ordinals. Ordinal.le : Ordinal β†’ Ordinal β†’ Prop
axiom_ordinal_lt_ty
Type of Ordinal.lt: strict ordering on ordinals. Ordinal.lt : Ordinal β†’ Ordinal β†’ Prop
axiom_ordinal_mul_ty
Type of Ordinal.mul: ordinal multiplication. Ordinal.mul : Ordinal β†’ Ordinal β†’ Ordinal
axiom_ordinal_omega_ty
Type of Ordinal.omega: the first infinite ordinal Ο‰. Ordinal.omega : Ordinal
axiom_ordinal_pow_ty
Type of Ordinal.pow: ordinal exponentiation. Ordinal.pow : Ordinal β†’ Ordinal β†’ Ordinal
axiom_ordinal_succ_ty
Type of Ordinal.succ: successor ordinal. Ordinal.succ : Ordinal β†’ Ordinal
axiom_ordinal_sup_ty
Type of Ordinal.sup: supremum of a set of ordinals. Ordinal.sup : (Nat β†’ Ordinal) β†’ Ordinal
axiom_ordinal_type_ty
Type of Ordinal: the type of ordinals. Ordinal : Type 1
axiom_ordinal_zero_ty
Type of Ordinal.zero: the ordinal zero. Ordinal.zero : Ordinal
axiom_partial_order_antisymmetry_ty
Type of PartialOrder.antisymmetry: a partial order is antisymmetric. PartialOrder.antisymmetry : βˆ€ {Ξ±} [PartialOrder Ξ±] (a b : Ξ±), a ≀ b β†’ b ≀ a β†’ a = b
axiom_ramsey_order_thm_ty
Type of Ramsey.orderThm: infinite Ramsey theorem for order relations. Ramsey.orderThm : Nat β†’ Nat β†’ Prop
axiom_rationals_universal_linear_order_ty
Type of Rationals.universalLinearOrder: the rationals form a universal homogeneous countable dense linear order without endpoints. Rationals.universalLinearOrder : Prop
axiom_regular_cardinal_ty
Type of RegularCardinal: a cardinal equal to its own cofinality. RegularCardinal : Ordinal β†’ Prop
axiom_suslin_problem_ty
Type of Suslin.problem: is every dense linear order without endpoints satisfying the countable chain condition isomorphic to the reals? Suslin.problem : Prop
axiom_total_order_linear_extension_ty
Type of TotalOrder.linearExtension: every partial order extends to a total order. TotalOrder.linearExtension : PartialOrder β†’ TotalOrder
axiom_well_order_induction_ty
Type of WellOrder.induction: transfinite induction for well-orders. WellOrder.induction : βˆ€ Ξ±, WellOrder Ξ± β†’ (βˆ€ x, (βˆ€ y, y < x β†’ P y) β†’ P x) β†’ βˆ€ x, P x
axiom_well_order_isomorphism_ty
Type of WellOrder.isomorphism: any two well-orders of the same ordinal are isomorphic. WellOrder.isomorphism : WellOrder β†’ WellOrder β†’ Prop
axiom_wqo_carrier_ty
Type of WQO.carrier: the carrier type of a well-quasi-order. WQO.carrier : WQO β†’ Type
axiom_wqo_le_ty
Type of WQO.le: the quasi-order relation. WQO.le : (w : WQO) β†’ WQO.carrier w β†’ WQO.carrier w β†’ Prop
axiom_wqo_wf_ty
Type of WQO.wf: every infinite sequence has a good pair. WQO.wf : (w : WQO) β†’ βˆ€ (f : Nat β†’ WQO.carrier w), βˆƒ i j, i < j ∧ WQO.le w (f i) (f j)
bool_cmp
Compare two bool values (false < true).
bottom_n
Return the bottom-n smallest elements of a slice, in increasing order.
build_full_ordering_env
Build a richer Ordering environment: add the Ord typeclass plus the Ordering comparators that depend on Bool.
build_ordering_env
Build Ordering type in the environment.
cmp
Compare two Ord values and return an Ordering.
cmp_by_key
Compare using a key function.
cmp_slices
Compare two slices lexicographically.
f64_cmp
Compare two f64 values (NaN is treated as Equal to itself, Less than everything else).
i64_cmp
Compare two i64 values.
is_sorted
true if a slice is sorted in non-decreasing order.
is_sorted_desc
true if a slice is sorted in non-increasing order.
kth_largest
Select the k-th largest element from a slice (0-indexed).
kth_smallest
Select the k-th smallest element from a slice (0-indexed).
lower_bound
Find the lower bound index for target in a sorted slice.
merge_sorted
Merge two sorted slices into a sorted Vec.
option_cmp
Lexicographic order on Option<T>: None < Some(x) for all x.
ord_ext_arrow
Helper: build Ξ± β†’ Ξ² as a Pi with anonymous binder.
ordering_chain
Chain a sequence of Ordering values (first non-Equal wins).
ordering_ge
true if a >= b.
ordering_gt
true if a > b.
ordering_le
true if a <= b.
ordering_lt
true if a < b (using Ordering).
ordering_max
Return the maximum of two values according to Ordering.
ordering_min
Return the minimum of two values according to Ordering.
register_ordering_extended
Register all extended ordering/ordinal axioms in the environment.
result_cmp
Lexicographic order on Result<T, E>: Err < Ok for distinct constructors.
sorted
Return a sorted copy of a slice.
sorted_by_key
Return a sorted copy using a key function.
sorted_desc
Return a reverse-sorted copy of a slice.
sorted_difference
Compute the sorted difference (a minus b) of two sorted slices.
sorted_intersection
Compute the sorted intersection of two sorted slices.
sorted_union
Compute the sorted union of two sorted slices (no duplicates).
str_cmp
Compare two &str values using the Ordering type.
top_n
Return the top-n largest elements of a slice, in decreasing order.
upper_bound
Find the upper bound index for target in a sorted slice.
usize_cmp
Compare two usize values.