Commit 2025-03-17 22:05 da2fde29

View on Github →

feat: restricted products and their topology (#20021)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/RestrictedProduct.lean

added theorem RestrictedProduct.continuous_coe

added theorem RestrictedProduct.continuous_dom

added theorem RestrictedProduct.continuous_dom_prod

added theorem RestrictedProduct.continuous_dom_prod_left

added theorem RestrictedProduct.continuous_dom_prod_right

added theorem RestrictedProduct.continuous_inclusion

added theorem RestrictedProduct.continuous_rng_of_bot

added theorem RestrictedProduct.continuous_rng_of_principal

added theorem RestrictedProduct.continuous_rng_of_top

added theorem RestrictedProduct.exists_inclusion_eq_of_eventually

added theorem RestrictedProduct.exists_structureMap_eq_of_forall

added def RestrictedProduct.homeoBot

added def RestrictedProduct.homeoTop

added def RestrictedProduct.inclusion

added theorem RestrictedProduct.inclusion_eq_id

added theorem RestrictedProduct.isEmbedding_coe_of_bot

added theorem RestrictedProduct.isEmbedding_coe_of_principal

added theorem RestrictedProduct.isEmbedding_coe_of_top

added theorem RestrictedProduct.isEmbedding_inclusion_principal

added theorem RestrictedProduct.isEmbedding_inclusion_top

added theorem RestrictedProduct.isEmbedding_structureMap

added theorem RestrictedProduct.isOpenEmbedding_inclusion_principal

added theorem RestrictedProduct.isOpenEmbedding_structureMap

added theorem RestrictedProduct.isOpen_forall_imp_mem

added theorem RestrictedProduct.isOpen_forall_imp_mem_of_principal

added theorem RestrictedProduct.isOpen_forall_mem

added theorem RestrictedProduct.isOpen_forall_mem_of_principal

added theorem RestrictedProduct.locallyCompactSpace_of_group

added theorem RestrictedProduct.nhds_eq_map_inclusion

added theorem RestrictedProduct.nhds_eq_map_structureMap

added theorem RestrictedProduct.nhds_zero_eq_map_ofPre

added theorem RestrictedProduct.nhds_zero_eq_map_structureMap

added theorem RestrictedProduct.range_coe

added theorem RestrictedProduct.range_coe_principal

added theorem RestrictedProduct.range_inclusion

added theorem RestrictedProduct.range_structureMap

added def RestrictedProduct.structureMap

added theorem RestrictedProduct.topologicalSpace_eq_iSup

added theorem RestrictedProduct.topologicalSpace_eq_of_bot

added theorem RestrictedProduct.topologicalSpace_eq_of_principal

added theorem RestrictedProduct.topologicalSpace_eq_of_top

added theorem RestrictedProduct.weaklyLocallyCompactSpace_of_cofinite

added theorem RestrictedProduct.weaklyLocallyCompactSpace_of_principal

added def RestrictedProduct