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 fieldsAlgebra.Order.Group.CompleteLattice
for distributivity of group operations over supremum/infimumAlgebra.Order.Group.Pointwise.Bounds
for boundedness of pointwise-defined setsAlgebra.Order.Group.Pointwise.CompleteLattice
for lemmas about the supremum/infimum of pointwise-defined sets.