Commit 2024-11-11 16:21 815b017f

View on Github →

chore(Algebra/InfiniteSum/Order): weaken typeclass assumptions (#18742) Generalise the typeclass assumptions on three lemmas, with no other changes.

  • Remove any assumptions relating the order and the algebra on hasProd_le_of_prod_le, also weaken OrderClosedTopology to ClosedIicTopology
  • Remove any assumptions relating the order and the algebra on le_hasProd_of_le_prod, also weaken OrderClosedTopology to ClosedIciTopology
  • Remove the T2 assumption on tprod_le_of_prod_range_le, also weaken OrderClosedTopology to ClosedIicTopology The first two changes mean these lemmas can now be used for infinite products of reals.

Estimated changes

modified theorem hasProd_le_of_prod_le
modified theorem le_hasProd_of_le_prod
modified theorem tprod_le_of_prod_range_le