Commit 2024-01-29 06:37 1fa9ebf0

feat(Algebra/InfiniteSum): drop [T2Space _] assumption (#10060)

• Add CanLift instance for Function.Embedding.
• Assume Injective i instead of an equivalent condition in hasSum_iff_hasSum_of_ne_zero_bij.
• Add tsum_eq_sum', a version of tsum_eq_sum that explicitly mentions support f.
• Add Function.Injective.tsum_eq, use it to drop [T2Space _] assumption in
  • Equiv.tsum_eq;
  • tsum_subtype_eq_of_support_subset;
  • tsum_subtype_support;
  • tsum_subtype;
  • tsum_univ;
  • tsum_image;
  • tsum_range;
  • tsum_setElem_eq_tsum_setElem_diff;
  • tsum_eq_tsum_diff_singleton;
  • tsum_eq_tsum_of_ne_zero_bij;
  • Equiv.tsum_eq_tsum_of_support;
  • tsum_extend_zero;
• Golf some proofs.
• Drop Equiv.Set.prod_singleton_left and Equiv.Set.prod_singleton_right added in #10038. @MichaelStollBayreuth, if you need these Equivs, then please
  • restore them in Logic/Equiv/Set, not in Data/Set/Prod;
  • call them Equiv.Set.singletonProd and Equiv.Set.prodSingleton, following the lowerCamelCase naming convention for defs;
  • reuse the existing Equiv.Set.prod and Equiv.prodUnique/Equiv.uniqueProd in the definitions.