ProperlyDiscontinuous

Statistics

Metric	Count
Definitions	0
Theorems `properlyDiscontinuousSMul_iff_properSMul`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`properlyDiscontinuousSMul_iff_properSMul` 📖	mathematical	—	`ProperlyDiscontinuousSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `ProperSMul`	—	`properSMul_iff` `isProperMap_iff_isCompact_preimage` `Prod.t2Space` `to_compactlyCoherentSpace` `Continuous.prodMk` `continuous_prod_of_discrete_left` `ContinuousConstSMul.continuous_const_smul` `Continuous.snd` `continuous_id'` `IsCompact.union` `IsCompact.image` `continuous_fst` `continuous_snd` `ProperlyDiscontinuousSMul.finite_disjoint_inter_image` `Set.ext` `Set.iUnion_congr_Prop` `Set.singleton_prod` `Set.iUnion_exists` `Set.biUnion_and'` `inv_smul_smul` `smul_inv_smul` `Set.Finite.isCompact_biUnion` `IsCompact.prod` `isCompact_singleton` `IsCompact.inter` `IsCompact.of_isClosed_subset` `IsClosed.preimage` `IsCompact.isClosed` `Set.preimage_mono` `IsCompact.finite_of_discrete` `IsProperMap.comp` `IsTopologicalGroup.toContinuousInv` `topologicalGroup_of_discreteTopology` `ProperSMul.isProperMap_smul_pair` `IsProperMap.prodMap` `Homeomorph.isProperMap` `isProperMap_id` `IsProperMap.isCompact_preimage`

---