Commit 2024-05-28 00:44 aba5b6ad

View on Github →

feat(Topology/Algebra/InfiniteSum/Order): Add tprod_subtype_le (#12600) We add a lemma that says the tprod/tsum over a subtype is less than the full sum. Needed for #12456

Estimated changes

added theorem tprod_subtype_le