Commit 2025-03-11 15:38 756396de

View on Github →

chore(Topology/Constructions): split out results about sums, products and distributivity (#22827) And move all homeomorphism related to direct sums, products and distributivity into the new file. This resolves a large file warning. It mostly reduces transitive imports (and causes mild increases in other places, and didn't import Homeomorph.Defs before). This is also necessary to break an import cycle in https://github.com/leanprover-community/mathlib4/pull/22137.

Estimated changes

deleted theorem Continuous.Prod.mk
deleted theorem Continuous.Prod.mk_left
deleted theorem Continuous.comp₂
deleted theorem Continuous.comp₃
deleted theorem Continuous.comp₄
deleted theorem Continuous.curry_left
deleted theorem Continuous.curry_right
deleted theorem Continuous.fst'
deleted theorem Continuous.fst
deleted theorem Continuous.prodMap
deleted theorem Continuous.prod_mk
deleted theorem Continuous.snd'
deleted theorem Continuous.snd
deleted theorem Continuous.sumElim
deleted theorem Continuous.sumMap
deleted theorem Continuous.uncurry_left
deleted theorem Continuous.uncurry_right
deleted theorem ContinuousAt.comp₂
deleted theorem ContinuousAt.fst''
deleted theorem ContinuousAt.fst'
deleted theorem ContinuousAt.fst
deleted theorem ContinuousAt.prod
deleted theorem ContinuousAt.prodMap'
deleted theorem ContinuousAt.prodMap
deleted theorem ContinuousAt.snd''
deleted theorem ContinuousAt.snd'
deleted theorem ContinuousAt.snd
deleted theorem Dense.prod
deleted theorem DenseRange.prodMap
deleted theorem Filter.HasBasis.prod_nhds
deleted theorem Filter.Tendsto.fst_nhds
deleted theorem Filter.Tendsto.snd_nhds
deleted theorem IsClosed.prod
deleted theorem IsClosed.setOf_mapsTo
deleted theorem IsClosedEmbedding.sumElim
deleted theorem IsClosedMap.sumElim
deleted theorem IsClosedMap.sumMap
deleted theorem IsOpen.prod
deleted theorem IsOpenEmbedding.sumElim
deleted theorem IsOpenMap.sumElim
deleted theorem IsOpenMap.sumMap
deleted theorem IsOpenQuotientMap.prodMap
deleted theorem Prod.tendsto_iff
deleted theorem closure_prod_eq
deleted theorem continuousAt_fst
deleted theorem continuousAt_snd
deleted theorem continuous_curry
deleted theorem continuous_fst
deleted theorem continuous_inl
deleted theorem continuous_inr
deleted theorem continuous_isLeft
deleted theorem continuous_isRight
deleted theorem continuous_prod_mk
deleted theorem continuous_sInf_dom₂
deleted theorem continuous_snd
deleted theorem continuous_sumElim
deleted theorem continuous_sumMap
deleted theorem continuous_sum_dom
deleted theorem continuous_sum_swap
deleted theorem continuous_swap
deleted theorem exists_nhds_square
deleted theorem frontier_prod_eq
deleted theorem frontier_prod_univ_eq
deleted theorem frontier_univ_prod_eq
deleted theorem interior_prod_eq
deleted theorem isClosedMap_inl
deleted theorem isClosedMap_inr
deleted theorem isClosedMap_sum
deleted theorem isClosedMap_sumElim
deleted theorem isClosedMap_swap
deleted theorem isClosed_range_inl
deleted theorem isClosed_range_inr
deleted theorem isClosed_sum_iff
deleted theorem isEmbedding_graph
deleted theorem isEmbedding_prodMk
deleted theorem isOpenMap_fst
deleted theorem isOpenMap_inl
deleted theorem isOpenMap_inr
deleted theorem isOpenMap_snd
deleted theorem isOpenMap_sum
deleted theorem isOpenMap_sumElim
deleted theorem isOpen_prod_iff'
deleted theorem isOpen_prod_iff
deleted theorem isOpen_range_inl
deleted theorem isOpen_range_inr
deleted theorem isOpen_sum_iff
deleted theorem isQuotientMap_fst
deleted theorem isQuotientMap_snd
deleted theorem map_fst_nhds
deleted theorem map_fst_nhdsWithin
deleted theorem map_mem_closure₂
deleted theorem map_snd_nhds
deleted theorem map_snd_nhdsWithin
deleted theorem mem_nhdsWithin_prod_iff
deleted theorem mem_nhds_prod_iff'
deleted theorem mem_nhds_prod_iff
deleted theorem nhdsWithin_prod_eq
deleted theorem nhds_inl
deleted theorem nhds_inr
deleted theorem nhds_prod_eq
deleted theorem nhds_swap
deleted theorem prod_eq_generateFrom
deleted theorem prod_induced_induced
deleted theorem prod_mem_nhds
deleted theorem prod_mem_nhds_iff
added theorem Continuous.Prod.mk
added theorem Continuous.comp₂
added theorem Continuous.comp₃
added theorem Continuous.comp₄
added theorem Continuous.curry_left
added theorem Continuous.curry_right
added theorem Continuous.fst'
added theorem Continuous.fst
added theorem Continuous.prodMap
added theorem Continuous.prod_mk
added theorem Continuous.snd'
added theorem Continuous.snd
added theorem Continuous.sumElim
added theorem Continuous.sumMap
added theorem ContinuousAt.comp₂
added theorem ContinuousAt.fst''
added theorem ContinuousAt.fst'
added theorem ContinuousAt.fst
added theorem ContinuousAt.prod
added theorem ContinuousAt.prodMap'
added theorem ContinuousAt.prodMap
added theorem ContinuousAt.snd''
added theorem ContinuousAt.snd'
added theorem ContinuousAt.snd
added theorem Dense.prod
added theorem DenseRange.prodMap
added theorem Homeomorph.coe_sumComm
added theorem IsClosed.prod
added theorem IsClosed.setOf_mapsTo
added theorem IsClosedMap.sumElim
added theorem IsClosedMap.sumMap
added theorem IsOpen.prod
added theorem IsOpenMap.sumElim
added theorem IsOpenMap.sumMap
added theorem Prod.tendsto_iff
added theorem closure_prod_eq
added theorem continuousAt_fst
added theorem continuousAt_snd
added theorem continuous_curry
added theorem continuous_fst
added theorem continuous_inl
added theorem continuous_inr
added theorem continuous_isLeft
added theorem continuous_isRight
added theorem continuous_prod_mk
added theorem continuous_sInf_dom₂
added theorem continuous_snd
added theorem continuous_sumElim
added theorem continuous_sumMap
added theorem continuous_sum_dom
added theorem continuous_sum_swap
added theorem continuous_swap
added theorem exists_nhds_square
added theorem frontier_prod_eq
added theorem frontier_prod_univ_eq
added theorem frontier_univ_prod_eq
added theorem interior_prod_eq
added theorem isClosedMap_inl
added theorem isClosedMap_inr
added theorem isClosedMap_sum
added theorem isClosedMap_sumElim
added theorem isClosedMap_swap
added theorem isClosed_range_inl
added theorem isClosed_range_inr
added theorem isClosed_sum_iff
added theorem isEmbedding_graph
added theorem isEmbedding_prodMk
added theorem isOpenMap_fst
added theorem isOpenMap_inl
added theorem isOpenMap_inr
added theorem isOpenMap_snd
added theorem isOpenMap_sum
added theorem isOpenMap_sumElim
added theorem isOpen_prod_iff'
added theorem isOpen_prod_iff
added theorem isOpen_range_inl
added theorem isOpen_range_inr
added theorem isOpen_sum_iff
added theorem isQuotientMap_fst
added theorem isQuotientMap_snd
added theorem map_fst_nhds
added theorem map_fst_nhdsWithin
added theorem map_mem_closure₂
added theorem map_snd_nhds
added theorem map_snd_nhdsWithin
added theorem mem_nhds_prod_iff'
added theorem mem_nhds_prod_iff
added theorem nhdsWithin_prod_eq
added theorem nhds_inl
added theorem nhds_inr
added theorem nhds_prod_eq
added theorem nhds_swap
added theorem prod_eq_generateFrom
added theorem prod_induced_induced
added theorem prod_mem_nhds
added theorem prod_mem_nhds_iff