Documentation Verification Report

Basic

📁 Source: Mathlib/Topology/Algebra/ProperAction/Basic.lean

Statistics

Metric	Count
Definitions `ProperSMul`, `ProperVAdd`	2
Theorems `smul_right_of_isCompact`, `vadd_right_of_isCompact`, `isProperMap_smul_pair`, `isProperMap_smul_pair_set`, `toContinuousSMul`, `isProperMap_vadd_pair`, `isProperMap_vadd_pair_set`, `toContinuousVAdd`, `instT2Space`, `instT2Space`, `instProperSMulMulOppositeOfIsTopologicalGroup`, `instProperSMulOfIsTopologicalGroup`, `instProperSMulSubtypeMemSubgroupOfIsClosedCoe`, `instProperSMulSubtypeMulOppositeMemSubgroupOpOfIsTopologicalGroupOfIsClosedCoe`, `instProperVAddAddOppositeOfIsTopologicalAddGroup`, `instProperVAddOfIsTopologicalAddGroup`, `instProperVAddSubtypeAddOppositeMemAddSubgroupOpOfIsTopologicalAddGroupOfIsClosedCoe`, `instProperVAddSubtypeMemAddSubgroupOfIsClosedCoe`, `properSMul_iff`, `properSMul_iff_continuousSMul_ultrafilter_tendsto`, `properSMul_iff_continuousSMul_ultrafilter_tendsto_t2`, `properSMul_of_isClosedEmbedding`, `properVAdd_iff`, `properVAdd_iff_continuousVAdd_ultrafilter_tendsto`, `properVAdd_of_isClosedEmbedding`, `t2Space_of_properSMul_of_t1Group`, `t2Space_of_properVAdd_of_t1AddGroup`, `t2Space_quotient_addAction_of_properVAdd`, `t2Space_quotient_mulAction_of_properSMul`	29
Total	31

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_right_of_isCompact` 📖	mathematical	`IsCompact`	`IsClosed` `Set` `Set.smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`ProperSMul.isProperMap_smul_pair_set` `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_fst_of_compactSpace` `preimage` `continuous_fst`
`vadd_right_of_isCompact` 📖	mathematical	`IsCompact`	`IsClosed` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vadd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`ProperVAdd.isProperMap_vadd_pair_set` `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_fst_of_compactSpace` `preimage` `continuous_fst`

ProperSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isProperMap_smul_pair` 📖	mathematical	—	`IsProperMap` `instTopologicalSpaceProd` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	—
`isProperMap_smul_pair_set` 📖	mathematical	—	`IsProperMap` `Set.Elem` `instTopologicalSpaceProd` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`isProperMap_smul_pair` `Set.ext` `Set.univ_prod` `IsProperMap.comp` `Homeomorph.isProperMap` `IsProperMap.restrictPreimage`
`toContinuousSMul` 📖	mathematical	—	`ContinuousSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Continuous.fst` `IsProperMap.continuous` `isProperMap_smul_pair`

ProperVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isProperMap_vadd_pair` 📖	mathematical	—	`IsProperMap` `instTopologicalSpaceProd` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	—
`isProperMap_vadd_pair_set` 📖	mathematical	—	`IsProperMap` `Set.Elem` `instTopologicalSpaceProd` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`isProperMap_vadd_pair` `Set.ext` `Set.mem_prod` `Set.mem_univ` `Set.mem_preimage` `Set.univ_prod` `IsProperMap.comp` `Homeomorph.isProperMap` `IsProperMap.restrictPreimage`
`toContinuousVAdd` 📖	mathematical	—	`ContinuousVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Continuous.fst` `IsProperMap.continuous` `isProperMap_vadd_pair`

QuotientAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instT2Space` 📖	mathematical	—	`T2Space` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `instTopologicalSpace`	—	`t2Space_quotient_addAction_of_properVAdd` `instProperVAddSubtypeAddOppositeMemAddSubgroupOpOfIsTopologicalAddGroupOfIsClosedCoe`

QuotientGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instT2Space` 📖	mathematical	—	`T2Space` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `instTopologicalSpace`	—	`t2Space_quotient_mulAction_of_properSMul` `instProperSMulSubtypeMulOppositeMemSubgroupOpOfIsTopologicalGroupOfIsClosedCoe`

(root)

Definitions

Name	Category	Theorems
`ProperSMul` 📖	CompData	9 math math: `properSMul_iff`, `instProperSMulOfIsTopologicalGroup`, `properSMul_of_isClosedEmbedding`, `properSMul_iff_continuousSMul_ultrafilter_tendsto_t2`, `instProperSMulSubtypeMulOppositeMemSubgroupOpOfIsTopologicalGroupOfIsClosedCoe`, `properSMul_iff_continuousSMul_ultrafilter_tendsto`, `instProperSMulMulOppositeOfIsTopologicalGroup`, `instProperSMulSubtypeMemSubgroupOfIsClosedCoe`, `properlyDiscontinuousSMul_iff_properSMul`
`ProperVAdd` 📖	CompData	8 math math: `instProperVAdd`, `properVAdd_of_isClosedEmbedding`, `instProperVAddSubtypeMemAddSubgroupOfIsClosedCoe`, `instProperVAddAddOppositeOfIsTopologicalAddGroup`, `properVAdd_iff`, `properVAdd_iff_continuousVAdd_ultrafilter_tendsto`, `instProperVAddSubtypeAddOppositeMemAddSubgroupOpOfIsTopologicalAddGroupOfIsClosedCoe`, `instProperVAddOfIsTopologicalAddGroup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instProperSMulMulOppositeOfIsTopologicalGroup` 📖	mathematical	—	`ProperSMul` `MulOpposite` `MulOpposite.instTopologicalSpaceMulOpposite` `MulOpposite.instGroup` `Monoid.toOppositeMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`inv_mul_cancel_left` `mul_inv_cancel_left` `Continuous.prodMk` `Continuous.fun_mul` `IsTopologicalGroup.toContinuousMul` `Continuous.snd` `continuous_id'` `Continuous.comp'` `MulOpposite.continuous_unop` `Continuous.fst` `MulOpposite.continuous_op` `Continuous.inv` `IsTopologicalGroup.toContinuousInv` `Homeomorph.isProperMap`
`instProperSMulOfIsTopologicalGroup` 📖	mathematical	—	`ProperSMul` `Monoid.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`mul_inv_cancel_right` `inv_mul_cancel_right` `Continuous.prodMk` `Continuous.fun_mul` `IsTopologicalGroup.toContinuousMul` `Continuous.fst` `continuous_id'` `Continuous.snd` `Continuous.inv` `IsTopologicalGroup.toContinuousInv` `Homeomorph.isProperMap`
`instProperSMulSubtypeMemSubgroupOfIsClosedCoe` 📖	mathematical	—	`ProperSMul` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `instTopologicalSpaceSubtype` `Subgroup.toGroup` `MulAction.instMulAction`	—	`properSMul_of_isClosedEmbedding` `IsClosed.isClosedEmbedding_subtypeVal`
`instProperSMulSubtypeMulOppositeMemSubgroupOpOfIsTopologicalGroupOfIsClosedCoe` 📖	mathematical	—	`ProperSMul` `MulOpposite` `Subgroup` `MulOpposite.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.op` `instTopologicalSpaceSubtype` `MulOpposite.instTopologicalSpaceMulOpposite` `Subgroup.toGroup` `MulAction.instMulAction` `Monoid.toOppositeMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`IsClosed.preimage` `MulOpposite.continuous_unop` `instProperSMulSubtypeMemSubgroupOfIsClosedCoe` `instProperSMulMulOppositeOfIsTopologicalGroup`
`instProperVAddAddOppositeOfIsTopologicalAddGroup` 📖	mathematical	—	`ProperVAdd` `AddOpposite` `AddOpposite.instTopologicalSpaceAddOpposite` `AddOpposite.instAddGroup` `AddMonoid.toOppositeAddAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`neg_add_cancel_left` `add_neg_cancel_left` `Continuous.prodMk` `Continuous.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `Continuous.snd` `continuous_id'` `Continuous.comp'` `AddOpposite.continuous_unop` `Continuous.fst` `AddOpposite.continuous_op` `Continuous.neg` `IsTopologicalAddGroup.toContinuousNeg` `Homeomorph.isProperMap`
`instProperVAddOfIsTopologicalAddGroup` 📖	mathematical	—	`ProperVAdd` `AddMonoid.toAddAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`add_neg_cancel_right` `neg_add_cancel_right` `Continuous.prodMk` `Continuous.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `Continuous.fst` `continuous_id'` `Continuous.snd` `Continuous.neg` `IsTopologicalAddGroup.toContinuousNeg` `Homeomorph.isProperMap`
`instProperVAddSubtypeAddOppositeMemAddSubgroupOpOfIsTopologicalAddGroupOfIsClosedCoe` 📖	mathematical	—	`ProperVAdd` `AddOpposite` `AddSubgroup` `AddOpposite.instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.op` `instTopologicalSpaceSubtype` `AddOpposite.instTopologicalSpaceAddOpposite` `AddSubgroup.toAddGroup` `AddAction.instAddAction` `AddMonoid.toOppositeAddAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`IsClosed.preimage` `AddOpposite.continuous_unop` `instProperVAddSubtypeMemAddSubgroupOfIsClosedCoe` `instProperVAddAddOppositeOfIsTopologicalAddGroup`
`instProperVAddSubtypeMemAddSubgroupOfIsClosedCoe` 📖	mathematical	—	`ProperVAdd` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `instTopologicalSpaceSubtype` `AddSubgroup.toAddGroup` `AddAction.instAddAction`	—	`properVAdd_of_isClosedEmbedding` `IsClosed.isClosedEmbedding_subtypeVal`
`properSMul_iff` 📖	mathematical	—	`ProperSMul` `IsProperMap` `instTopologicalSpaceProd` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	—
`properSMul_iff_continuousSMul_ultrafilter_tendsto` 📖	mathematical	—	`ProperSMul` `ContinuousSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Filter.Tendsto` `Ultrafilter.toFilter` `nhds`	—	`ProperSMul.toContinuousSMul` `isProperMap_iff_ultrafilter` `properSMul_iff` `Filter.Tendsto.mono_left` `Continuous.tendsto` `continuous_fst` `Continuous.prodMk` `Continuous.smul` `Continuous.fst` `continuous_id'` `Continuous.snd` `nhds_prod_eq` `Filter.le_prod` `Filter.Tendsto.comp` `continuous_snd`
`properSMul_iff_continuousSMul_ultrafilter_tendsto_t2` 📖	mathematical	—	`ProperSMul` `ContinuousSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Filter.Tendsto` `Ultrafilter.toFilter` `nhds`	—	`properSMul_iff_continuousSMul_ultrafilter_tendsto` `tendsto_nhds_unique` `Ultrafilter.neBot` `Filter.Tendsto.smul` `Filter.Tendsto.comp` `Continuous.tendsto` `continuous_snd` `continuous_fst`
`properSMul_of_isClosedEmbedding` 📖	mathematical	`Topology.IsClosedEmbedding` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	`ProperSMul`	—	`IsProperMap.prodMap` `Topology.IsClosedEmbedding.isProperMap` `isProperMap_id` `IsProperMap.comp` `ProperSMul.isProperMap_smul_pair`
`properVAdd_iff` 📖	mathematical	—	`ProperVAdd` `IsProperMap` `instTopologicalSpaceProd` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	—
`properVAdd_iff_continuousVAdd_ultrafilter_tendsto` 📖	mathematical	—	`ProperVAdd` `ContinuousVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `HVAdd.hVAdd` `instHVAdd` `Filter.Tendsto` `Ultrafilter.toFilter` `nhds`	—	`ProperVAdd.toContinuousVAdd` `isProperMap_iff_ultrafilter` `properVAdd_iff` `Filter.Tendsto.mono_left` `Continuous.tendsto` `continuous_fst` `Continuous.prodMk` `Continuous.vadd` `Continuous.fst` `continuous_id'` `Continuous.snd` `nhds_prod_eq` `Filter.le_prod` `Filter.Tendsto.comp` `continuous_snd`
`properVAdd_of_isClosedEmbedding` 📖	mathematical	`Topology.IsClosedEmbedding` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction`	`ProperVAdd`	—	`IsProperMap.prodMap` `Topology.IsClosedEmbedding.isProperMap` `isProperMap_id` `IsProperMap.comp` `ProperVAdd.isProperMap_vadd_pair`
`t2Space_of_properSMul_of_t1Group` 📖	mathematical	—	`T2Space`	—	`Topology.IsClosedEmbedding.isProperMap` `Function.LeftInverse.isEmbedding` `Continuous.snd` `continuous_id'` `Continuous.prodMk` `continuous_const` `Set.singleton_prod` `Set.image_univ` `IsClosed.prod` `isClosed_singleton` `isClosed_univ` `t2_iff_isClosed_diagonal` `properSMul_iff` `one_smul` `Set.range_diag` `IsProperMap.isClosed_range` `IsProperMap.comp`
`t2Space_of_properVAdd_of_t1AddGroup` 📖	mathematical	—	`T2Space`	—	`Topology.IsClosedEmbedding.isProperMap` `Function.LeftInverse.isEmbedding` `Continuous.snd` `continuous_id'` `Continuous.prodMk` `continuous_const` `Set.singleton_prod` `Set.image_univ` `IsClosed.prod` `isClosed_singleton` `isClosed_univ` `t2_iff_isClosed_diagonal` `properVAdd_iff` `zero_vadd` `Set.range_diag` `IsProperMap.isClosed_range` `IsProperMap.comp`
`t2Space_quotient_addAction_of_properVAdd` 📖	mathematical	—	`T2Space` `AddAction.orbitRel` `instTopologicalSpaceQuotient`	—	`t2_iff_isClosed_diagonal` `IsOpenQuotientMap.prodMap` `AddAction.isOpenQuotientMap_quotientMk` `ContinuousVAdd.continuousConstVAdd` `ProperVAdd.toContinuousVAdd` `Topology.IsQuotientMap.isClosed_preimage` `IsOpenQuotientMap.isQuotientMap` `Set.ext` `Set.mem_preimage` `Set.mem_diagonal_iff` `Set.mem_range` `Quotient.eq'` `AddAction.orbitRel_apply` `AddAction.mem_orbit_iff` `IsClosedMap.isClosed_range` `IsProperMap.isClosedMap` `ProperVAdd.isProperMap_vadd_pair`
`t2Space_quotient_mulAction_of_properSMul` 📖	mathematical	—	`T2Space` `MulAction.orbitRel` `instTopologicalSpaceQuotient`	—	`t2_iff_isClosed_diagonal` `IsOpenQuotientMap.prodMap` `MulAction.isOpenQuotientMap_quotientMk` `ContinuousSMul.continuousConstSMul` `ProperSMul.toContinuousSMul` `Topology.IsQuotientMap.isClosed_preimage` `IsOpenQuotientMap.isQuotientMap` `Set.ext` `Quotient.eq'` `MulAction.orbitRel_apply` `MulAction.mem_orbit_iff` `IsClosedMap.isClosed_range` `IsProperMap.isClosedMap` `ProperSMul.isProperMap_smul_pair`

---

← Back to Index