Commit 2025-03-16 23:10 9130de84

View on Github →

chore(*): rename lots of theorems (#22195) Normalize prod_mk -> prodMk and prod_map -> prodMap in lemma names.

Estimated changes

deleted theorem Filter.mem_comap_prod_mk
added theorem Filter.Tendsto.prodMap
added theorem Filter.Tendsto.prodMk
deleted theorem Filter.Tendsto.prod_map
deleted theorem Filter.Tendsto.prod_mk
added theorem HasProd.prodMk
deleted theorem HasProd.prod_mk
deleted theorem Continuous.Prod.mk
deleted theorem Continuous.Prod.mk_left
added theorem Continuous.prodMk
added theorem Continuous.prodMk_left
deleted theorem Continuous.prod_mk
deleted theorem ContinuousAt.prod
added theorem ContinuousAt.prodMk
added theorem continuous_prodMk
deleted theorem continuous_prod_mk
deleted theorem ContinuousOn.prod
added theorem ContinuousOn.prodMap
added theorem ContinuousOn.prodMk
deleted theorem ContinuousOn.prod_map
deleted theorem ContinuousWithinAt.prod
deleted theorem IsLocallyConstant.prod_mk
deleted theorem UniformContinuous.prod_mk
deleted theorem CauchySeq.prod
added theorem CauchySeq.prodMap
added theorem CauchySeq.prodMk
deleted theorem CauchySeq.prod_map
added theorem prodMk_mem_compRel
deleted theorem prod_mk_mem_compRel
deleted theorem TendstoUniformly.prod
deleted theorem TendstoUniformly.prod_map