bend-mathlib
Search uses release 0.8.1.0 · 1,126 definitions
Definitions (1,126)
- law add_lt_add_iff_left_symAdding the same amount on the left does not change the strict order test: a < b tests as k + a < k + b, reversed to rewrite toward the simple side.
- law add_lt_add_iff_right_symAdding the same amount on the right does not change the strict order test: a < b tests as a + k < b + k, reversed to rewrite toward the simple side.
- law min_max_distrib_left_symMinimum distributes over maximum on the left: min a (max b c) = max (min a b) (min a c), reversed to rewrite toward the simple side.
- law max_min_distrib_left_symMaximum distributes over minimum on the left: max a (min b c) = min (max a b) (max a c), reversed to rewrite toward the simple side.
- law min_add_add_left_symA common left summand leaves the minimum: min (a + b) (a + c) = a + min b c, reversed to rewrite toward the simple side.
- law min_add_add_right_symA common right summand leaves the minimum: min (a + c) (b + c) = min a b + c, reversed to rewrite toward the simple side.
- law max_add_add_left_symA common left summand leaves the maximum: max (a + b) (a + c) = a + max b c, reversed to rewrite toward the simple side.
- law max_add_add_right_symA common right summand leaves the maximum: max (a + c) (b + c) = max a b + c, reversed to rewrite toward the simple side.
- law min_lt_iff_symThe minimum is below c exactly when one argument is: min a b < c tests as a < c or b < c, reversed to rewrite toward the simple side.
- law lt_min_iff_symA number is below the minimum exactly when it is below both: a < min b c tests as a < b and a < c, reversed to rewrite toward the simple side.
- law max_lt_iff_symThe maximum is below c exactly when both arguments are: max a b < c tests as a < c and b < c, reversed to rewrite toward the simple side.
- law le_max_iff_symA number is at most the maximum exactly when it is at most one argument: a <= max b c tests as a <= b or a <= c, reversed to rewrite toward the simple side.
- law add_mul_div_right_symAdding a multiple of a positive divisor adds to the quotient: (x + z * (1 + b)) / (1 + b) = x / (1 + b) + z, reversed to rewrite toward the simple side.
- law add_mul_div_left_symAdding a multiple of a positive divisor adds to the quotient: (x + (1 + b) * z) / (1 + b) = x / (1 + b) + z, reversed to rewrite toward the simple side.
- law add_mul_mod_self_right_symAdding a multiple of the divisor keeps the remainder: (a + c * b) % b = a % b, reversed to rewrite toward the simple side.
- law add_mul_mod_self_left_symAdding a multiple of the divisor keeps the remainder: (a + b * c) % b = a % b, reversed to rewrite toward the simple side.
- law mod_two_eq_zero_or_one_symA remainder modulo two is zero or one, reversed to rewrite toward the simple side.
- law div_add_mod_symThe divisor times the quotient plus the remainder is the dividend: b * (a / b) + a % b = a, reversed to rewrite toward the simple side.
- law two_mul_symTwo times n is n + n, reversed to rewrite toward the simple side.
- law double_eq_two_mul_symDoubling is multiplying by two: double n = 2 * n, reversed to rewrite toward the simple side.
- law double_add_symDoubling distributes over addition: double (a + b) = double a + double b, reversed to rewrite toward the simple side.
- law double_mul_symDoubling a product doubles its left factor: double (a * b) = double a * b, reversed to rewrite toward the simple side.
- law mul_double_symMultiplying by a doubled factor doubles the product: a * double b = double (a * b), reversed to rewrite toward the simple side.
- law double_sub_symDoubling distributes over truncated subtraction: double (a - b) = double a - double b, reversed to rewrite toward the simple side.
- law double_div_two_add_mod_two_symTwice the half plus the parity is the number: double (n / 2) + n % 2 = n, reversed to rewrite toward the simple side.
- law add_le_add_iff_right_symAdding the same amount on the right does not change the order test: a <= b tests as a + k <= b + k, reversed to rewrite toward the simple side.
- law add_left_cancel_iff_symAdding the same amount on the left does not change the equality test: a = b tests as k + a = k + b, reversed to rewrite toward the simple side.
- law add_right_cancel_iff_symAdding the same amount on the right does not change the equality test: a = b tests as a + k = b + k, reversed to rewrite toward the simple side.
- law mul_two_symMultiplying n by two gives n + n, reversed to rewrite toward the simple side.
- law pow_two_symSquaring n gives n times n, reversed to rewrite toward the simple side.
- law min_le_max_symThe minimum of two numbers is at most their maximum, reversed to rewrite toward the simple side.
- law two_pow_succ_symTwo to a successor power is double the power: 2^(n+1) = double (2^n), reversed to rewrite toward the simple side.
- def internal_shift
- def internal_apply_app
- def internal_apply_shift
- def perm_reflPermutation is reflexive.
- def perm_nilThe empty list is a permutation of itself.
- def perm_swapSwapping the two leading elements is a permutation.
- def internal_trans_eq
- def perm_transPermutation is transitive.
- def internal_cons_eq
- def perm_consPrepending the same element preserves permutation.
- def perm_dupA Perm hypothesis in existential form is reusable.
- def insert_byInsertion into a list, generic comparator (structural, Base-only branching via Bool.pick).
- def isort_byInsertion sort by the comparator le.
- def internal_ins_pick
- def insert_by_permInserting x into xs permutes x <> xs.
- def isort_by_permInsertion sort permutes its input.
- def isort_by_perm_natInsertion sort permutes a Nat list.
- def internal_append_nil
- def perm_append_nilAppending Nil is a permutation, by the empty step list.
- def perm_moveMoving an element from the middle to the front is a permutation.
- def merge_byMerges two lists, taking the head of xs first whenever le(x, y) holds.
- def internal_merge_pick
- def merge_by_permMerging permutes the concatenation.
- def merge_by_perm_natMerging two Nat lists permutes their concatenation.
- def perm_move_revMoving the front element into the middle is a permutation.
- def perm_append_commAppending commutes up to permutation (derived without symmetry).
- def perm_append_rightPermuting the right operand of an append gives a permutation of the append.
- def perm_appendPermuting both operands of an append gives a permutation of the append.
- def evensThe elements of a list at even positions (0, 2, 4, ...).
- def oddsThe elements of a list at odd positions (1, 3, 5, ...).
- def split_permSplitting into evens and odds is a permutation.
- def msort_byMerge sort with fuel (the fuel only bounds recursion; it never affects the permutation).
- def msort_by_permMerge sort permutes its input, for any fuel.
- def sort_byMerge sort by the comparator le.
- def sort_by_permThe sort permutes its input.
- def sort_by_perm_natMerge sort permutes a Nat list.
- def internal_sort_nat_test
- def internal_swap_head_invol
- def internal_swap_at_invol
- def internal_invert
- def internal_apply_invert
- def internal_sym_eq
- def perm_symPermutation is symmetric.
- def internal_swap_head_length
- def internal_swap_at_length
- def internal_apply_length
- def internal_length_eq
- def perm_lengthPermutation preserves length.