Commit 2023-06-27 14:42 8a1d3524

View on Github →

fix: precedence for finprod/finsum (#5524)

Replace notation3 lines with the latest versions in mathport.
Fix Topology.PartitionOfUnity.
Fix names in Topology.PartitionOfUnity (locally_finite' -> locallyFinite').
Use FunLike for PartitionOfUnity and BumpCovering

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finprod.lean

Modified Mathlib/Topology/PartitionOfUnity.lean

added theorem BumpCovering.continuous_toPOUFun

deleted theorem BumpCovering.continuous_toPouFun

added theorem BumpCovering.exists_finset_toPOUFun_eventuallyEq

deleted theorem BumpCovering.exists_finset_toPouFun_eventuallyEq

added theorem BumpCovering.sum_toPOUFun_eq

deleted theorem BumpCovering.sum_toPouFun_eq

added theorem BumpCovering.support_toPOUFun_subset

deleted theorem BumpCovering.support_toPouFun_subset

added def BumpCovering.toPOUFun

added theorem BumpCovering.toPOUFun_eq_mul_prod

added theorem BumpCovering.toPOUFun_zero_of_zero

deleted def BumpCovering.toPouFun

deleted theorem BumpCovering.toPouFun_eq_mul_prod

deleted theorem BumpCovering.toPouFun_zero_of_zero