bend-mathlib
Search uses release 0.8.1.0 · 1,126 definitions
Definitions (1,126)
- law mul_right_commRight commutativity of multiplication: (a * b) * c = (a * c) * b.
- law mul_mul_mul_commFour-way regrouping of a product: (a * b) * (c * d) = (a * c) * (b * d).
- law zero_powZero to a positive power is zero: 0^(n+1) = 0.
- law mul_powA power of a product is the product of the powers: (a * b)^n = a^n * b^n.
- law pow_mulExponents multiply under repeated powers: a^(m * n) = (a^m)^n.
- law one_le_powA power of a positive base is at least one: 1 <= (1 + a)^n.
- law pow_posA power of a positive base is positive: 0 < (1 + a)^n.
- law le_add_leftAdding on the left never decreases a natural: n <= m + n.
- law add_sub_add_leftA common left summand cancels in a difference: (k + n) - (k + m) = n - m.
- law add_sub_add_rightA common right summand cancels in a difference: (n + k) - (m + k) = n - m.
- law add_sub_assocSubtracting a part of the right summand: k <= m implies (n + m) - k = n + (m - k).
- law sub_sub_selfSubtracting a difference from its minuend: m <= n implies n - (n - m) = m.
- law sub_mulMultiplication distributes over subtraction on the right: (n - m) * k = n * k - m * k.
- law mul_subMultiplication distributes over subtraction on the left: n * (m - k) = n * m - n * k.
- law min_eq_leftThe minimum is the smaller argument on the left: a <= b implies min a b = a.
- law min_eq_rightThe minimum is the smaller argument on the right: b <= a implies min a b = b.
- law max_eq_leftThe maximum is the larger argument on the left: b <= a implies max a b = a.
- law max_eq_rightThe maximum is the larger argument on the right: a <= b implies max a b = b.
- def internal_and_false_sym
- def internal_and_true_sym
- law le_minA number is at most the minimum exactly when it is at most both: a <= min b c tests as a <= b and a <= c (Mathlib's le_min_iff; the implication is le_min_of_le_of_le).
- law max_leThe maximum is at most c exactly when both arguments are: max a b <= c tests as a <= c and b <= c (Mathlib's max_le_iff; the implication is max_le_of_le_of_le).
- law mul_le_mul_leftMultiplying on the left preserves the order: a <= b implies k * a <= k * b.
- law mul_le_mulMultiplying two bounded factors stays bounded: a <= c and b <= d imply a * b <= c * d.
- law succ_posEvery successor is positive: 0 < n + 1.
- law lt_succ_iffBelow a successor means at most: m < n + 1 tests as m <= n.
- law succ_lt_succThe successor preserves the strict order: a < b implies a + 1 < b + 1.
- law lt_of_succ_lt_succThe strict order of successors is the strict order of the naturals: a + 1 < b + 1 implies a < b.
- law le_of_lt_succBelow a successor is at most: m < n + 1 implies m <= n.
- law lt_succ_of_leAt most is below the successor: m <= n implies m < n + 1.
- law succ_le_of_ltA strict inequality gives the weak one from the successor: n < m implies n + 1 <= m.
- law lt_of_succ_leA weak inequality from the successor gives the strict one: n + 1 <= m implies n < m.
- law lt_asymmThe strict order is asymmetric: a < b rules out b < a.
- law le_iff_lt_or_eqAt most means below or equal: a <= b tests as a < b or a = b.
- law lt_iff_le_and_neBelow means at most and different: a < b tests as a <= b and not a = b.
- law pos_of_ne_zeroA natural that does not test equal to zero is positive.
- law lt_add_rightAdding on the right keeps a strict bound: n < m implies n < m + k.
- law lt_add_of_pos_rightAdding a positive amount on the right strictly increases: n < n + (1 + k).
- law lt_add_of_pos_leftAdding a positive amount on the left strictly increases: n < (1 + k) + n.
- law add_lt_add_leftAdding on the left preserves the strict order: a < b implies k + a < k + b.
- law add_lt_add_rightAdding on the right preserves the strict order: a < b implies a + k < b + k.
- law add_lt_add_iff_leftAdding the same amount on the left does not change the strict order test: a < b tests as k + a < k + b.
- law add_lt_add_iff_rightAdding the same amount on the right does not change the strict order test: a < b tests as a + k < b + k.
- law lt_of_add_lt_add_leftA common left summand cancels in a strict inequality: k + a < k + b implies a < b.
- law lt_of_add_lt_add_rightA common right summand cancels in a strict inequality: a + k < b + k implies a < b.
- law add_lt_addAdding two strict bounds keeps a strict bound: a < c and b < d imply a + b < c + d.
- law le_mul_of_pos_leftA positive left factor never decreases: m <= (1 + n) * m.
- law le_mul_of_pos_rightA positive right factor never decreases: m <= m * (1 + n).
- law mul_lt_mul_of_pos_leftMultiplying on the left by a positive factor preserves the strict order: a < b implies (1 + k) * a < (1 + k) * b.
- law mul_lt_mul_of_pos_rightMultiplying on the right by a positive factor preserves the strict order: a < b implies a * (1 + k) < b * (1 + k).
- def internal_lt_of_not_le
- law lt_of_mul_lt_mul_leftA common left factor cancels in a strict inequality: k * a < k * b implies a < b.
- law lt_of_mul_lt_mul_rightA common right factor cancels in a strict inequality: a * k < b * k implies a < b.
- law mul_lt_mul_of_lt_of_ltMultiplying two strict bounds keeps a strict bound: a < c and b < d imply a * b < c * d.
- law mul_self_le_mul_selfSquares are monotone: a <= b implies a * a <= b * b.
- law mul_self_lt_mul_selfSquares are strictly monotone: a < b implies a * a < b * b.
- law sub_ltSubtracting a positive amount from a positive number decreases it: (1 + n) - (1 + m) < 1 + n.
- law sub_le_sub_leftSubtracting more gives less: n <= m implies k - m <= k - n.
- law sub_le_sub_rightSubtraction on the right preserves the order: n <= m implies n - k <= m - k.
- law lt_sub_of_add_ltA strict bound on a sum bounds a difference: a + b < c implies a < c - b.
- law sub_pos_of_ltA difference is positive below the minuend: m < n implies 0 < n - m.
- law min_max_distrib_leftMinimum distributes over maximum on the left: min a (max b c) = max (min a b) (min a c).
- law max_min_distrib_leftMaximum distributes over minimum on the left: max a (min b c) = min (max a b) (max a c).
- law min_add_add_leftA common left summand leaves the minimum: min (a + b) (a + c) = a + min b c.
- law min_add_add_rightA common right summand leaves the minimum: min (a + c) (b + c) = min a b + c.
- law max_add_add_leftA common left summand leaves the maximum: max (a + b) (a + c) = a + max b c.
- law max_add_add_rightA common right summand leaves the maximum: max (a + c) (b + c) = max a b + c.
- law min_lt_iffThe minimum is below c exactly when one argument is: min a b < c tests as a < c or b < c.
- law lt_min_iffA number is below the minimum exactly when it is below both: a < min b c tests as a < b and a < c.
- law max_lt_iffThe maximum is below c exactly when both arguments are: max a b < c tests as a < c and b < c.
- law le_max_iffA 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.
- law le_max_of_le_leftA bound by the left argument bounds the maximum: a <= b implies a <= max b c.
- law le_max_of_le_rightA bound by the right argument bounds the maximum: a <= c implies a <= max b c.
- law min_le_of_left_leA bounded left argument bounds the minimum: a <= c implies min a b <= c.
- law min_le_of_right_leA bounded right argument bounds the minimum: b <= c implies min a b <= c.
- law min_le_minMinimum is monotone in both arguments: a <= c and b <= d imply min a b <= min c d.
- law max_le_maxMaximum is monotone in both arguments: a <= c and b <= d imply max a b <= max c d.
- law pow_le_pow_leftPowers are monotone in the base: a <= b implies a^n <= b^n.
- law pow_le_pow_rightPowers of a positive base are monotone in the exponent: i <= j implies (1 + a)^i <= (1 + a)^j.
- def internal_lt_mul_two_add
- law pow_lt_pow_rightPowers of a base above one are strictly monotone in the exponent: i < j implies (2 + a)^i < (2 + a)^j.
- law pow_lt_pow_leftPositive powers are strictly monotone in the base: a < b implies a^(1 + n) < b^(1 + n).
- law add_mul_div_rightAdding a multiple of a positive divisor adds to the quotient: (x + z * (1 + b)) / (1 + b) = x / (1 + b) + z.
- law add_mul_div_leftAdding a multiple of a positive divisor adds to the quotient: (x + (1 + b) * z) / (1 + b) = x / (1 + b) + z.
- law div_le_div_leftDivision is antitone in a positive divisor: 0 < s and s <= t imply a / t <= a / s.
- law add_mul_mod_self_rightAdding a multiple of the divisor keeps the remainder: (a + c * b) % b = a % b.
- law add_mul_mod_self_leftAdding a multiple of the divisor keeps the remainder: (a + b * c) % b = a % b.
- def internal_lt_one_succ
- def internal_lt_two
- law mod_two_eq_zero_or_oneA remainder modulo two is zero or one.
- law div_add_modThe divisor times the quotient plus the remainder is the dividend: b * (a / b) + a % b = a.
- law two_mulTwo times n is n + n.
- law double_eq_two_mulDoubling is multiplying by two: double n = 2 * n.
- law double_addDoubling distributes over addition: double (a + b) = double a + double b.
- law double_mulDoubling a product doubles its left factor: double (a * b) = double a * b.
- law mul_doubleMultiplying by a doubled factor doubles the product: a * double b = double (a * b).
- law double_subDoubling distributes over truncated subtraction: double (a - b) = double a - double b.
- law le_doubleA natural is at most its double: n <= double n.
- law double_le_doubleDoubling preserves the order: a <= b implies double a <= double b.
- law double_lt_doubleDoubling preserves the strict order: a < b implies double a < double b.