Commit 2024-09-26 00:42 9678fd7f

View on Github →

chore: split Algebra.Bounds and Algebra.Order.Pointwise (#16986) Delete Algebra.Bounds and Algebra.Order.Pointwise. Create

  • Algebra.Order.Field.Pointwise for lemmas about pointwise operations in linear ordered fields
  • Algebra.Order.Group.CompleteLattice for distributivity of group operations over supremum/infimum
  • Algebra.Order.Group.Pointwise.Bounds for boundedness of pointwise-defined sets
  • Algebra.Order.Group.Pointwise.CompleteLattice for lemmas about the supremum/infimum of pointwise-defined sets.

Estimated changes

deleted theorem BddAbove.inv
deleted theorem BddAbove.mul
deleted theorem BddAbove.range_inv
deleted theorem BddAbove.range_mul
deleted theorem BddBelow.inv
deleted theorem BddBelow.mul
deleted theorem BddBelow.range_inv
deleted theorem BddBelow.range_mul
deleted theorem IsGLB.inv
deleted theorem IsLUB.inv
deleted theorem bddAbove_inv
deleted theorem bddBelow_inv
deleted theorem ciInf_div
deleted theorem ciInf_mul
deleted theorem ciSup_div
deleted theorem ciSup_mul
deleted theorem isGLB_inv'
deleted theorem isGLB_inv
deleted theorem isLUB_inv'
deleted theorem isLUB_inv
deleted theorem mul_ciInf
deleted theorem mul_ciSup
deleted theorem mul_mem_lowerBounds_mul
deleted theorem mul_mem_upperBounds_mul
deleted theorem subset_lowerBounds_mul
deleted theorem subset_upperBounds_mul
added theorem ciInf_div
added theorem ciInf_mul
added theorem ciSup_div
added theorem ciSup_mul
added theorem mul_ciInf
added theorem mul_ciSup
added theorem BddAbove.inv
added theorem BddAbove.mul
added theorem BddAbove.range_inv
added theorem BddAbove.range_mul
added theorem BddBelow.inv
added theorem BddBelow.mul
added theorem BddBelow.range_inv
added theorem BddBelow.range_mul
added theorem IsGLB.inv
added theorem IsLUB.inv
added theorem bddAbove_inv
added theorem bddBelow_inv
added theorem isGLB_inv'
added theorem isGLB_inv
added theorem isLUB_inv'
added theorem isLUB_inv
added theorem subset_lowerBounds_mul
added theorem subset_upperBounds_mul
added theorem csInf_div
added theorem csInf_inv
added theorem csInf_mul
added theorem csInf_one
added theorem csSup_div
added theorem csSup_inv
added theorem csSup_mul
added theorem csSup_one
added theorem sInf_div
added theorem sInf_inv
added theorem sInf_mul
added theorem sInf_one
added theorem sSup_div
added theorem sSup_inv
added theorem sSup_mul
added theorem sSup_one
deleted theorem csInf_div
deleted theorem csInf_inv
deleted theorem csInf_mul
deleted theorem csInf_one
deleted theorem csSup_div
deleted theorem csSup_inv
deleted theorem csSup_mul
deleted theorem csSup_one
deleted theorem sInf_div
deleted theorem sInf_inv
deleted theorem sInf_mul
deleted theorem sInf_one
deleted theorem sSup_div
deleted theorem sSup_inv
deleted theorem sSup_mul
deleted theorem sSup_one