CompactlyGenerated

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

Statistics

Metric	Count
Definitions	0
Theorems properVAdd_iff_isCompact_setOf_inter_nonempty, properSMul_iff_isCompact_setOf_inter_nonempty, properlyDiscontinuousSMul_iff_properSMul, properlyDiscontinuousVAdd_iff_properVAdd	4
Total	4

AddAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
properVAdd_iff_isCompact_setOf_inter_nonempty 📖	mathematical	—	ProperVAdd IsCompact setOf Set.Nonempty Set Set.instInter HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction	—	ProperVAdd.isCompact_setOf_inter_nonempty isProperMap_iff_isCompact_preimage Prod.t2Space to_compactlyCoherentSpace Continuous.prodMk Continuous.vadd Continuous.fst continuous_id' Continuous.snd IsCompact.image continuous_fst continuous_snd IsCompact.of_isClosed_subset IsCompact.prod IsClosed.preimage IsCompact.isClosed Set.vadd_mem_vadd_set Set.preimage_mono Set.subset_fst_image_prod_snd_image

MulAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
properSMul_iff_isCompact_setOf_inter_nonempty 📖	mathematical	—	ProperSMul IsCompact setOf Set.Nonempty Set Set.instInter Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction	—	ProperSMul.isCompact_setOf_inter_nonempty isProperMap_iff_isCompact_preimage Prod.t2Space to_compactlyCoherentSpace Continuous.prodMk Continuous.smul Continuous.fst continuous_id' Continuous.snd IsCompact.image continuous_fst continuous_snd IsCompact.of_isClosed_subset IsCompact.prod IsClosed.preimage IsCompact.isClosed Set.smul_mem_smul_set Set.preimage_mono Set.subset_fst_image_prod_snd_image

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
properlyDiscontinuousSMul_iff_properSMul 📖	mathematical	—	ProperlyDiscontinuousSMul SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction ProperSMul	—	continuous_prod_of_discrete_left ContinuousConstSMul.continuous_const_smul properlyDiscontinuousSMul_iff
properlyDiscontinuousVAdd_iff_properVAdd 📖	mathematical	—	ProperlyDiscontinuousVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction ProperVAdd	—	continuous_prod_of_discrete_left ContinuousConstVAdd.continuous_const_vadd AddAction.properVAdd_iff_isCompact_setOf_inter_nonempty isCompact_iff_finite properlyDiscontinuousVAdd_iff

---

← Back to Index