Commit 2023-02-21 20:43 e7e49c8a

View on Github →

feat: port Topology.Algebra.Group.Basic (#2267)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Group/Basic.lean

added structure AddGroupTopology

added theorem Continuous.div'

added theorem Continuous.inv

added theorem Continuous.zpow

added theorem ContinuousAt.div'

added theorem ContinuousAt.inv

added theorem ContinuousAt.zpow

added theorem ContinuousInv.of_nhds_one

added theorem ContinuousOn.div'

added theorem ContinuousOn.inv

added theorem ContinuousOn.zpow

added theorem ContinuousWithinAt.div'

added theorem ContinuousWithinAt.inv

added theorem ContinuousWithinAt.zpow

added theorem DenseRange.topologicalClosure_map_subgroup

added theorem Filter.HasBasis.nhds_of_one

added theorem Filter.Tendsto.const_div'

added theorem Filter.Tendsto.div'

added theorem Filter.Tendsto.div_const'

added theorem Filter.Tendsto.inv

added theorem Filter.Tendsto.zpow

added def GroupTopology.coinduced

added theorem GroupTopology.coinduced_continuous

added theorem GroupTopology.continuous_inv'

added theorem GroupTopology.continuous_mul'

added theorem GroupTopology.ext'

added theorem GroupTopology.toTopologicalSpace_bot

added theorem GroupTopology.toTopologicalSpace_inf

added theorem GroupTopology.toTopologicalSpace_infᵢ

added theorem GroupTopology.toTopologicalSpace_infₛ

added theorem GroupTopology.toTopologicalSpace_injective

added theorem GroupTopology.toTopologicalSpace_le

added theorem GroupTopology.toTopologicalSpace_top

added structure GroupTopology

added theorem Homeomorph.coe_mulLeft

added theorem Homeomorph.coe_mulRight

added def Homeomorph.divLeft

added def Homeomorph.divRight

added theorem Homeomorph.mulLeft_symm

added theorem Homeomorph.mulRight_symm

added theorem Homeomorph.shearMulRight_coe

added theorem Homeomorph.shearMulRight_symm_coe

added theorem Inducing.continuousInv

added theorem IsClosed.inv

added theorem IsClosed.leftCoset

added theorem IsClosed.rightCoset

added theorem IsCompact.inv

added theorem IsOpen.closure_div

added theorem IsOpen.closure_mul

added theorem IsOpen.div_closure

added theorem IsOpen.div_left

added theorem IsOpen.div_right

added theorem IsOpen.inv

added theorem IsOpen.leftCoset

added theorem IsOpen.mul_closure

added theorem IsOpen.mul_left

added theorem IsOpen.mul_right

added theorem IsOpen.rightCoset

added theorem IsOpen.smul_left

added theorem QuotientGroup.continuous_smul₁

added theorem QuotientGroup.isOpenMap_coe

added theorem QuotientGroup.nhds_eq

added def Subgroup.commGroupTopologicalClosure

added def Subgroup.connectedComponentOfOne

added theorem Subgroup.isClosed_topologicalClosure

added theorem Subgroup.is_normal_topologicalClosure

added theorem Subgroup.le_topologicalClosure

added theorem Subgroup.properlyDiscontinuousSMul_of_tendsto_cofinite

added theorem Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite

added def Subgroup.topologicalClosure

added theorem Subgroup.topologicalClosure_coe

added theorem Subgroup.topologicalClosure_minimal

added theorem TopologicalGroup.continuous_conj'

added theorem TopologicalGroup.continuous_conj

added theorem TopologicalGroup.continuous_conj_prod

added theorem TopologicalGroup.exists_antitone_basis_nhds_one

added theorem TopologicalGroup.ext

added theorem TopologicalGroup.ext_iff

added theorem TopologicalGroup.of_comm_of_nhds_one

added theorem TopologicalGroup.of_nhds_one'

added theorem TopologicalGroup.of_nhds_one

added theorem TopologicalGroup.t1Space

added theorem TopologicalGroup.t2Space

added theorem TopologicalGroup.t3Space

added def Units.Homeomorph.prodUnits

added theorem compact_covered_by_mul_left_translates

added theorem compact_open_separated_mul_left

added theorem compact_open_separated_mul_right

added theorem continuousAt_inv

added theorem continuousAt_zpow

added theorem continuousInv_inf

added theorem continuousInv_infᵢ

added theorem continuousInv_infₛ

added theorem continuousOn_inv

added theorem continuousOn_zpow

added theorem continuousWithinAt_inv

added theorem continuous_div_left'

added theorem continuous_div_right'

added theorem continuous_of_continuousAt_one

added theorem continuous_zpow

added theorem discreteTopology_iff_open_singleton_one

added theorem discreteTopology_of_open_singleton_one

added theorem exists_disjoint_smul_of_isCompact

added theorem exists_nhds_split_inv

added theorem inv_closure

added theorem inv_mem_connectedComponent_one

added theorem inv_mem_nhds_one

added theorem isClosedMap_div_left

added theorem isClosedMap_div_right

added theorem isClosedMap_inv

added theorem isClosedMap_mul_left

added theorem isClosedMap_mul_right

added theorem isClosed_setOf_map_inv

added theorem isOpenMap_div_left

added theorem isOpenMap_div_right

added theorem isOpenMap_inv

added theorem isOpenMap_mul_left

added theorem isOpenMap_mul_right

added theorem local_isCompact_isClosed_nhds_of_group

added theorem map_mul_left_nhds

added theorem map_mul_left_nhds_one

added theorem map_mul_right_nhds

added theorem map_mul_right_nhds_one

added theorem mem_closure_iff_nhds_one

added theorem mul_mem_connectedComponent_one

added theorem mul_singleton_mem_nhds

added theorem mul_singleton_mem_nhds_of_nhds_one

added def nhdsMulHom

added theorem nhds_mul

added theorem nhds_one_symm'

added theorem nhds_one_symm

added theorem nhds_translation_div

added theorem nhds_translation_mul_inv

added theorem singleton_mul_mem_nhds

added theorem singleton_mul_mem_nhds_of_nhds_one

added theorem smul_mem_nhds

added theorem subset_interior_div

added theorem subset_interior_div_left

added theorem subset_interior_div_right

added theorem subset_interior_mul'

added theorem subset_interior_mul

added theorem subset_interior_mul_left

added theorem subset_interior_mul_right

added theorem subset_interior_smul

added theorem subset_interior_smul_right

added theorem tendsto_div_nhds_one_iff

added theorem tendsto_inv

added theorem tendsto_inv_nhdsWithin_Ici

added theorem tendsto_inv_nhdsWithin_Ici_inv

added theorem tendsto_inv_nhdsWithin_Iic

added theorem tendsto_inv_nhdsWithin_Iic_inv

added theorem tendsto_inv_nhdsWithin_Iio

added theorem tendsto_inv_nhdsWithin_Iio_inv

added theorem tendsto_inv_nhdsWithin_Ioi

added theorem tendsto_inv_nhdsWithin_Ioi_inv

added theorem topologicalGroup_induced

added theorem topologicalGroup_inf

added theorem topologicalGroup_infᵢ

added theorem topologicalGroup_infₛ

Modified Mathlib/Topology/Constructions.lean

modified theorem Continuous.quotient_map'