Pointwise

📁 Source: Mathlib/Topology/Algebra/Group/Pointwise.lean

Statistics

Metric	Count
Definitions	0
Theorems `isClosedMap_quotient`, `eq_zero_or_locallyCompactSpace_of_addGroup`, `eq_zero_or_locallyCompactSpace_of_group`, `add_closure_zero_eq`, `add_left_of_isCompact`, `add_right_of_isCompact`, `mul_closure_one_eq`, `mul_left_of_isCompact`, `mul_right_of_isCompact`, `smul_left_of_isCompact`, `vadd_left_of_isCompact`, `add_closure_zero_eq_closure`, `locallyCompactSpace_of_mem_nhds_of_addGroup`, `locallyCompactSpace_of_mem_nhds_of_group`, `mul_closure_one_eq_closure`, `exists_nhds_eq_one_of_image_mulLeft_inter_nonempty`, `exists_nhds_eq_one_of_image_mulRight_inter_nonempty`, `exists_nhds_eq_zero_of_image_addLeft_inter_nonempty`, `exists_nhds_eq_zero_of_image_addRight_inter_nonempty`, `add_closure`, `add_closure_zero_eq`, `add_left`, `add_right`, `closure_add`, `closure_div`, `closure_mul`, `closure_sub`, `div_closure`, `div_left`, `div_right`, `mul_closure`, `mul_closure_one_eq`, `mul_left`, `mul_right`, `sub_closure`, `sub_left`, `sub_right`, `regularSpace`, `t2Space_iff_zero_closed`, `t2Space_of_zero_sep`, `regularSpace`, `t2Space_iff_one_closed`, `t2Space_of_one_sep`, `isClosedMap_quotient`, `addGroup_inseparable_iff`, `add_singleton_mem_nhds`, `add_singleton_mem_nhds_of_nhds_zero`, `compl_add_closure_zero_eq`, `compl_add_closure_zero_eq_iff`, `compl_mul_closure_one_eq`, `compl_mul_closure_one_eq_iff`, `eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup`, `eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group`, `exists_closed_nhds_one_inv_eq_mul_subset`, `exists_closed_nhds_zero_neg_eq_add_subset`, `group_inseparable_iff`, `mul_singleton_mem_nhds`, `mul_singleton_mem_nhds_of_nhds_one`, `singleton_add_mem_nhds`, `singleton_add_mem_nhds_of_nhds_zero`, `singleton_mul_mem_nhds`, `singleton_mul_mem_nhds_of_nhds_one`, `subset_add_closure_zero`, `subset_interior_add`, `subset_interior_add'`, `subset_interior_add_left`, `subset_interior_add_right`, `subset_interior_div`, `subset_interior_div_left`, `subset_interior_div_right`, `subset_interior_mul`, `subset_interior_mul'`, `subset_interior_mul_left`, `subset_interior_mul_right`, `subset_interior_smul`, `subset_interior_sub`, `subset_interior_sub_left`, `subset_interior_sub_right`, `subset_interior_vadd`, `subset_mul_closure_one`	80
Total	80

AddAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosedMap_quotient` 📖	mathematical	—	`IsClosedMap` `orbitRel` `instTopologicalSpaceQuotient`	—	`Topology.IsQuotientMap.isClosed_preimage` `isQuotientMap_quotient_mk'` `quotient_preimage_image_eq_union_add` `Set.biUnion_univ` `Set.iUnion_vadd_left_image` `Set.iUnion_congr_Prop` `IsClosed.vadd_left_of_isCompact` `isCompact_univ`

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_or_locallyCompactSpace_of_addGroup` 📖	mathematical	`HasCompactSupport` `Continuous`	`Pi.instZero` `LocallyCompactSpace`	—	`eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup` `subset_tsupport`
`eq_zero_or_locallyCompactSpace_of_group` 📖	mathematical	`HasCompactSupport` `Continuous`	`Pi.instZero` `LocallyCompactSpace`	—	`eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group` `subset_tsupport`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_closure_zero_eq` 📖	mathematical	—	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `closure` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Set.Subset.antisymm` `closure_eq` `vadd_set_closure_subset` `ContinuousAdd.to_continuousVAdd` `IsTopologicalAddGroup.toContinuousAdd` `Set.add_singleton` `Set.image_congr` `add_zero` `Set.image_id'` `subset_add_closure_zero`
`add_left_of_isCompact` 📖	mathematical	`IsCompact`	`IsClosed` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`vadd_left_of_isCompact` `IsTopologicalAddGroup.toContinuousNeg` `ContinuousAdd.to_continuousVAdd` `IsTopologicalAddGroup.toContinuousAdd`
`add_right_of_isCompact` 📖	mathematical	`IsCompact`	`IsClosed` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`Set.image_op_vadd` `vadd_left_of_isCompact` `instContinuousNegAddOpposite` `IsTopologicalAddGroup.toContinuousNeg` `ContinuousAdd.to_continuousVAdd_op` `IsTopologicalAddGroup.toContinuousAdd` `IsCompact.image` `AddOpposite.continuous_op`
`mul_closure_one_eq` 📖	mathematical	—	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `closure` `Set.instSingletonSet` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Set.Subset.antisymm` `closure_eq` `smul_set_closure_subset` `ContinuousMul.to_continuousSMul` `IsTopologicalGroup.toContinuousMul` `Set.mul_singleton` `Set.image_congr` `mul_one` `Set.image_id'` `subset_mul_closure_one`
`mul_left_of_isCompact` 📖	mathematical	`IsCompact`	`IsClosed` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`smul_left_of_isCompact` `IsTopologicalGroup.toContinuousInv` `ContinuousMul.to_continuousSMul` `IsTopologicalGroup.toContinuousMul`
`mul_right_of_isCompact` 📖	mathematical	`IsCompact`	`IsClosed` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Set.image_op_smul` `smul_left_of_isCompact` `instContinuousInvMulOpposite` `IsTopologicalGroup.toContinuousInv` `ContinuousMul.to_continuousSMul_op` `IsTopologicalGroup.toContinuousMul` `IsCompact.image` `MulOpposite.continuous_op`
`smul_left_of_isCompact` 📖	mathematical	`IsCompact`	`IsClosed` `Set` `Set.smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`inv_smul_smul` `smul_inv_smul` `Continuous.prodMk` `Continuous.fst` `continuous_id'` `Continuous.smul` `Continuous.comp'` `continuous_subtype_val` `Continuous.snd` `Continuous.inv` `subset_antisymm` `Set.instAntisymmSubset` `Set.smul_subset_iff` `Set.mem_image_of_mem` `Set.image_subset_iff` `Set.smul_mem_smul` `isCompact_iff_compactSpace` `IsProperMap.isClosedMap` `IsProperMap.comp` `isProperMap_snd_of_compactSpace` `Homeomorph.isProperMap` `preimage` `continuous_snd`
`vadd_left_of_isCompact` 📖	mathematical	`IsCompact`	`IsClosed` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vadd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`neg_vadd_vadd` `vadd_neg_vadd` `Continuous.prodMk` `Continuous.fst` `continuous_id'` `Continuous.vadd` `Continuous.comp'` `continuous_subtype_val` `Continuous.snd` `Continuous.neg` `subset_antisymm` `Set.instAntisymmSubset` `Set.vadd_subset_iff` `Set.mem_image_of_mem` `Set.image_subset_iff` `Set.vadd_mem_vadd` `isCompact_iff_compactSpace` `IsProperMap.isClosedMap` `IsProperMap.comp` `isProperMap_snd_of_compactSpace` `Homeomorph.isProperMap` `preimage` `continuous_snd`

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_closure_zero_eq_closure` 📖	mathematical	`IsCompact`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `closure` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Set.Subset.antisymm` `Set.vadd_subset_vadd_right` `subset_closure` `vadd_set_closure_subset` `ContinuousAdd.to_continuousVAdd` `IsTopologicalAddGroup.toContinuousAdd` `Set.add_singleton` `Set.image_congr` `add_zero` `Set.image_id'` `IsClosed.vadd_left_of_isCompact` `IsTopologicalAddGroup.toContinuousNeg` `isClosed_closure` `IsClosed.closure_subset_iff` `subset_add_closure_zero`
`locallyCompactSpace_of_mem_nhds_of_addGroup` 📖	mathematical	`IsCompact` `Set` `Filter` `Filter.instMembership` `nhds`	`LocallyCompactSpace`	—	`vadd` `VAddAssocClass.continuousConstVAdd` `VAddAssocClass.left` `IsTopologicalAddGroup.toContinuousAdd` `Set.preimage_vadd_neg` `ContinuousAt.preimage_mem_nhds` `Continuous.continuousAt` `ContinuousConstVAdd.continuous_const_vadd` `neg_add_rev` `neg_neg` `neg_add_cancel_right` `WeaklyLocallyCompactSpace.locallyCompactSpace` `instR1Space` `IsTopologicalAddGroup.regularSpace`
`locallyCompactSpace_of_mem_nhds_of_group` 📖	mathematical	`IsCompact` `Set` `Filter` `Filter.instMembership` `nhds`	`LocallyCompactSpace`	—	`smul` `IsScalarTower.continuousConstSMul` `IsScalarTower.left` `IsTopologicalGroup.toContinuousMul` `Set.preimage_smul_inv` `ContinuousAt.preimage_mem_nhds` `Continuous.continuousAt` `ContinuousConstSMul.continuous_const_smul` `mul_inv_rev` `inv_inv` `inv_mul_cancel_right` `WeaklyLocallyCompactSpace.locallyCompactSpace` `instR1Space` `IsTopologicalGroup.regularSpace`
`mul_closure_one_eq_closure` 📖	mathematical	`IsCompact`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `closure` `Set.instSingletonSet` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Set.Subset.antisymm` `Set.smul_subset_smul_right` `subset_closure` `smul_set_closure_subset` `ContinuousMul.to_continuousSMul` `IsTopologicalGroup.toContinuousMul` `Set.mul_singleton` `Set.image_congr` `mul_one` `Set.image_id'` `IsClosed.smul_left_of_isCompact` `IsTopologicalGroup.toContinuousInv` `isClosed_closure` `IsClosed.closure_subset_iff` `subset_mul_closure_one`

IsDiscrete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_nhds_eq_one_of_image_mulLeft_inter_nonempty` 📖	mathematical	`IsDiscrete` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Set` `Filter` `Filter.instMembership` `nhds` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Set.inv` `InvOneClass.toInv`	—	`nhds_inter_eq_singleton_of_mem_discrete` `Subgroup.one_mem` `exists_closed_nhds_one_inv_eq_mul_subset` `Eq.subset` `Set.instReflSubset` `mul_inv_cancel_right`
`exists_nhds_eq_one_of_image_mulRight_inter_nonempty` 📖	mathematical	`IsDiscrete` `SetLike.coe` `Subgroup` `Subgroup.instSetLike`	`Set` `Filter` `Filter.instMembership` `nhds` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Set.inv` `InvOneClass.toInv`	—	`exists_nhds_eq_one_of_image_mulLeft_inter_nonempty` `inv_eq_one` `Subgroup.inv_mem` `Set.nonempty_image_mulLeft_inv_inter_iff`
`exists_nhds_eq_zero_of_image_addLeft_inter_nonempty` 📖	mathematical	`IsDiscrete` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`Set` `Filter` `Filter.instMembership` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Set.neg` `NegZeroClass.toNeg`	—	`nhds_inter_eq_singleton_of_mem_discrete` `AddSubgroup.zero_mem` `exists_closed_nhds_zero_neg_eq_add_subset` `Eq.subset` `Set.instReflSubset` `add_neg_cancel_right`
`exists_nhds_eq_zero_of_image_addRight_inter_nonempty` 📖	mathematical	`IsDiscrete` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	`Set` `Filter` `Filter.instMembership` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Set.neg` `NegZeroClass.toNeg`	—	`exists_nhds_eq_zero_of_image_addLeft_inter_nonempty` `neg_eq_zero` `AddSubgroup.neg_mem` `Set.nonempty_image_addLeft_neg_inter_iff`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_closure` 📖	mathematical	`IsOpen`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `closure`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Set.add_subset_iff` `Set.neg_mem_neg` `neg_add_cancel_left` `mem_closure_iff` `add_right` `VAddCommClass.continuousConstVAdd` `AddSemigroup.opposite_vaddCommClass` `IsTopologicalAddGroup.toContinuousAdd` `neg` `IsTopologicalAddGroup.toContinuousNeg` `Set.add_subset_add_left` `subset_closure`
`add_closure_zero_eq` 📖	mathematical	`IsOpen`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `closure` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`compl_add_closure_zero_eq_iff` `IsClosed.add_closure_zero_eq` `isClosed_compl`
`add_left` 📖	mathematical	`IsOpen`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`vadd_left`
`add_right` 📖	mathematical	`IsOpen`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`Set.image_op_vadd` `vadd_left`
`closure_add` 📖	mathematical	`IsOpen`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `closure`	—	`neg_neg` `neg_add_rev` `neg_closure` `IsTopologicalAddGroup.toContinuousNeg` `add_closure` `neg`
`closure_div` 📖	mathematical	`IsOpen`	`Set` `Set.div` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `closure`	—	`div_eq_mul_inv` `closure_mul` `inv` `IsTopologicalGroup.toContinuousInv`
`closure_mul` 📖	mathematical	`IsOpen`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `closure`	—	`inv_inv` `mul_inv_rev` `inv_closure` `IsTopologicalGroup.toContinuousInv` `mul_closure` `inv`
`closure_sub` 📖	mathematical	`IsOpen`	`Set` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `closure`	—	`sub_eq_add_neg` `closure_add` `neg` `IsTopologicalAddGroup.toContinuousNeg`
`div_closure` 📖	mathematical	`IsOpen`	`Set` `Set.div` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `closure`	—	`div_eq_mul_inv` `inv_closure` `IsTopologicalGroup.toContinuousInv` `mul_closure`
`div_left` 📖	mathematical	`IsOpen`	`Set` `Set.div` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`Set.iUnion_div_left_image` `isOpen_biUnion` `isOpenMap_div_left`
`div_right` 📖	mathematical	`IsOpen`	`Set` `Set.div` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`Set.iUnion_div_right_image` `isOpen_biUnion` `isOpenMap_div_right`
`mul_closure` 📖	mathematical	`IsOpen`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `closure`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Set.mul_subset_iff` `Set.inv_mem_inv` `inv_mul_cancel_left` `mem_closure_iff` `mul_right` `SMulCommClass.continuousConstSMul` `Semigroup.opposite_smulCommClass` `IsTopologicalGroup.toContinuousMul` `inv` `IsTopologicalGroup.toContinuousInv` `Set.mul_subset_mul_left` `subset_closure`
`mul_closure_one_eq` 📖	mathematical	`IsOpen`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `closure` `Set.instSingletonSet` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`compl_mul_closure_one_eq_iff` `IsClosed.mul_closure_one_eq` `isClosed_compl`
`mul_left` 📖	mathematical	`IsOpen`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`smul_left`
`mul_right` 📖	mathematical	`IsOpen`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Set.image_op_smul` `smul_left`
`sub_closure` 📖	mathematical	`IsOpen`	`Set` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `closure`	—	`sub_eq_add_neg` `neg_closure` `IsTopologicalAddGroup.toContinuousNeg` `add_closure`
`sub_left` 📖	mathematical	`IsOpen`	`Set` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`Set.iUnion_sub_left_image` `isOpen_biUnion` `isOpenMap_sub_left`
`sub_right` 📖	mathematical	`IsOpen`	`Set` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`Set.iUnion_sub_right_image` `isOpen_biUnion` `isOpenMap_sub_right`

IsTopologicalAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`regularSpace` 📖	mathematical	—	`RegularSpace`	—	`RegularSpace.of_exists_mem_nhds_isClosed_subset` `Continuous.tendsto'` `continuous_add` `toContinuousAdd` `add_zero` `mem_nhds_prod_iff` `Filter.mem_of_superset` `subset_closure` `isClosed_closure` `Set.subset_add_left` `mem_interior_iff_mem_nhds` `IsOpen.closure_add` `isOpen_interior` `Set.add_subset_add_left` `interior_subset` `Set.image_prod` `Set.image_subset_iff`
`t2Space_iff_zero_closed` 📖	mathematical	—	`T2Space` `IsClosed` `Set` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`isClosed_singleton` `T2Space.t1Space` `t1Space` `toContinuousAdd` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `T1Space.t0Space` `regularSpace`
`t2Space_of_zero_sep` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Set.instMembership`	`T2Space`	—	`t1Space_iff_specializes_imp_eq` `by_contra` `add_neg_eq_zero` `mem_of_mem_nhds` `Specializes.map` `continuous_add_right` `toContinuousAdd` `add_neg_cancel` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `T1Space.t0Space` `regularSpace`

IsTopologicalGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`regularSpace` 📖	mathematical	—	`RegularSpace`	—	`RegularSpace.of_exists_mem_nhds_isClosed_subset` `Continuous.tendsto'` `continuous_mul` `toContinuousMul` `mul_one` `mem_nhds_prod_iff` `Filter.mem_of_superset` `subset_closure` `isClosed_closure` `Set.subset_mul_left` `mem_interior_iff_mem_nhds` `IsOpen.closure_mul` `isOpen_interior` `Set.mul_subset_mul_left` `interior_subset` `Set.image_prod` `Set.image_subset_iff`
`t2Space_iff_one_closed` 📖	mathematical	—	`T2Space` `IsClosed` `Set` `Set.instSingletonSet` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`isClosed_singleton` `T2Space.t1Space` `t1Space` `toContinuousMul` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `T1Space.t0Space` `regularSpace`
`t2Space_of_one_sep` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Set.instMembership`	`T2Space`	—	`t1Space_iff_specializes_imp_eq` `by_contra` `mul_inv_eq_one` `mem_of_mem_nhds` `Specializes.map` `continuous_mul_right` `toContinuousMul` `mul_inv_cancel` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `T1Space.t0Space` `regularSpace`

MulAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosedMap_quotient` 📖	mathematical	—	`IsClosedMap` `orbitRel` `instTopologicalSpaceQuotient`	—	`Topology.IsQuotientMap.isClosed_preimage` `isQuotientMap_quotient_mk'` `quotient_preimage_image_eq_union_mul` `Set.biUnion_univ` `Set.iUnion_smul_left_image` `Set.iUnion_congr_Prop` `IsClosed.smul_left_of_isCompact` `isCompact_univ`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addGroup_inseparable_iff` 📖	mathematical	—	`Inseparable` `Set` `Set.instMembership` `closure` `Set.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`Set.singleton_zero` `specializes_iff_mem_closure` `specializes_comm` `instR0Space` `instR1Space` `IsTopologicalAddGroup.regularSpace` `specializes_iff_inseparable` `IsTopologicalAddGroup.toContinuousAdd` `Topology.IsInducing.inseparable_iff` `Topology.IsEmbedding.toIsInducing` `Homeomorph.isEmbedding` `add_neg_cancel` `sub_eq_add_neg`
`add_singleton_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Set.add` `Set.instSingletonSet`	—	`Set.add_singleton` `vadd_mem_nhds_vadd`
`add_singleton_mem_nhds_of_nhds_zero` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Set.instSingletonSet`	—	`zero_add` `add_singleton_mem_nhds`
`compl_add_closure_zero_eq` 📖	mathematical	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `closure` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`Compl.compl` `Set.instCompl`	—	`Set.Subset.antisymm` `AddSubgroup.coe_topologicalClosure_bot` `Set.mem_compl_iff` `AddSubgroup.neg_mem` `add_neg_cancel_right` `subset_add_closure_zero`
`compl_add_closure_zero_eq_iff` 📖	mathematical	—	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Compl.compl` `Set.instCompl` `closure` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`compl_compl` `compl_add_closure_zero_eq`
`compl_mul_closure_one_eq` 📖	mathematical	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `closure` `Set.instSingletonSet` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`Compl.compl` `Set.instCompl`	—	`Set.Subset.antisymm` `Subgroup.coe_topologicalClosure_bot` `Subgroup.inv_mem` `mul_inv_cancel_right` `subset_mul_closure_one`
`compl_mul_closure_one_eq_iff` 📖	mathematical	—	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Compl.compl` `Set.instCompl` `closure` `Set.instSingletonSet` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`compl_compl` `compl_mul_closure_one_eq`
`eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup` 📖	mathematical	`IsCompact` `Set` `Set.instHasSubset` `Function.support` `Continuous`	`Pi.instZero` `LocallyCompactSpace`	—	`Mathlib.Tactic.Push.not_forall_eq` `Filter.mem_of_superset` `IsOpen.mem_nhds` `Continuous.isOpen_support` `IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup`
`eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group` 📖	mathematical	`IsCompact` `Set` `Set.instHasSubset` `Function.support` `Continuous`	`Pi.instZero` `LocallyCompactSpace`	—	`Mathlib.Tactic.Push.not_forall_eq` `Filter.mem_of_superset` `IsOpen.mem_nhds` `Continuous.isOpen_support` `IsCompact.locallyCompactSpace_of_mem_nhds_of_group`
`exists_closed_nhds_one_inv_eq_mul_subset` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`IsClosed` `Set.inv` `InvOneClass.toInv` `Set.instHasSubset` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`exists_open_nhds_one_mul_subset` `IsTopologicalGroup.toContinuousMul` `exists_mem_nhds_isClosed_subset` `IsTopologicalGroup.regularSpace` `IsOpen.mem_nhds` `Filter.inter_mem` `inv_mem_nhds_one` `IsClosed.inter` `IsClosed.inv` `IsTopologicalGroup.toContinuousInv` `Set.inter_inv` `inv_inv` `Set.inter_comm` `Set.mul_subset_mul` `Set.inter_subset_left`
`exists_closed_nhds_zero_neg_eq_add_subset` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`IsClosed` `Set.neg` `NegZeroClass.toNeg` `Set.instHasSubset` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`exists_open_nhds_zero_add_subset` `IsTopologicalAddGroup.toContinuousAdd` `exists_mem_nhds_isClosed_subset` `IsTopologicalAddGroup.regularSpace` `IsOpen.mem_nhds` `Filter.inter_mem` `neg_mem_nhds_zero` `IsClosed.inter` `IsClosed.neg` `IsTopologicalAddGroup.toContinuousNeg` `Set.inter_neg` `neg_neg` `Set.inter_comm` `Set.add_subset_add` `Set.inter_subset_left`
`group_inseparable_iff` 📖	mathematical	—	`Inseparable` `Set` `Set.instMembership` `closure` `Set.one` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`Set.singleton_one` `specializes_iff_mem_closure` `specializes_comm` `instR0Space` `instR1Space` `IsTopologicalGroup.regularSpace` `specializes_iff_inseparable` `IsTopologicalGroup.toContinuousMul` `Topology.IsInducing.inseparable_iff` `Topology.IsEmbedding.toIsInducing` `Homeomorph.isEmbedding` `mul_inv_cancel` `div_eq_mul_inv`
`mul_singleton_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set.mul` `Set.instSingletonSet`	—	`Set.mul_singleton` `smul_mem_nhds_smul`
`mul_singleton_mem_nhds_of_nhds_one` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set.instSingletonSet`	—	`one_mul` `mul_singleton_mem_nhds`
`singleton_add_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Set.add` `Set.instSingletonSet`	—	`vadd_eq_add` `Set.singleton_vadd` `vadd_mem_nhds_vadd_iff`
`singleton_add_mem_nhds_of_nhds_zero` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Set.instSingletonSet`	—	`add_zero` `singleton_add_mem_nhds`
`singleton_mul_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set.mul` `Set.instSingletonSet`	—	`smul_eq_mul` `Set.singleton_smul` `smul_mem_nhds_smul_iff`
`singleton_mul_mem_nhds_of_nhds_one` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set.instSingletonSet`	—	`mul_one` `singleton_mul_mem_nhds`
`subset_add_closure_zero` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `closure` `Set.instSingletonSet` `AddZero.toZero`	—	`Set.add_singleton` `Set.image_congr` `add_zero` `Set.image_id'` `subset_refl` `Set.instReflSubset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.vadd_subset_vadd_left` `subset_closure`
`subset_interior_add` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `interior`	—	`subset_interior_vadd`
`subset_interior_add'` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `interior`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.add_subset_add_left` `interior_subset` `subset_interior_add_left`
`subset_interior_add_left` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `interior`	—	`interior_maximal` `Set.add_subset_add_right` `interior_subset` `IsOpen.add_right` `isOpen_interior`
`subset_interior_add_right` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `interior`	—	`subset_interior_vadd_right`
`subset_interior_div` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.div` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `interior`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.div_subset_div_left` `interior_subset` `subset_interior_div_left`
`subset_interior_div_left` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.div` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `interior`	—	`interior_maximal` `Set.div_subset_div_right` `interior_subset` `IsOpen.div_right` `isOpen_interior`
`subset_interior_div_right` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.div` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `interior`	—	`interior_maximal` `Set.div_subset_div_left` `interior_subset` `IsOpen.div_left` `isOpen_interior`
`subset_interior_mul` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `interior`	—	`subset_interior_smul`
`subset_interior_mul'` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `interior`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.mul_subset_mul_left` `interior_subset` `subset_interior_mul_left`
`subset_interior_mul_left` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `interior`	—	`interior_maximal` `Set.mul_subset_mul_right` `interior_subset` `IsOpen.mul_right` `isOpen_interior`
`subset_interior_mul_right` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `interior`	—	`subset_interior_smul_right`
`subset_interior_smul` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `interior`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.smul_subset_smul_right` `interior_subset` `subset_interior_smul_right`
`subset_interior_sub` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `interior`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.sub_subset_sub_left` `interior_subset` `subset_interior_sub_left`
`subset_interior_sub_left` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `interior`	—	`interior_maximal` `Set.sub_subset_sub_right` `interior_subset` `IsOpen.sub_right` `isOpen_interior`
`subset_interior_sub_right` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `interior`	—	`interior_maximal` `Set.sub_subset_sub_left` `interior_subset` `IsOpen.sub_left` `isOpen_interior`
`subset_interior_vadd` 📖	mathematical	—	`Set` `Set.instHasSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vadd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `interior`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.vadd_subset_vadd_right` `interior_subset` `subset_interior_vadd_right`
`subset_mul_closure_one` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `closure` `Set.instSingletonSet` `MulOne.toOne`	—	`Set.mul_singleton` `Set.image_congr` `mul_one` `Set.image_id'` `Set.instReflSubset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.smul_subset_smul_left` `subset_closure`

---

← Back to Index