CompactlyGenerated

📁 Source: Mathlib/Topology/Maps/Proper/CompactlyGenerated.lean

Statistics

Metric	Count
Definitions CompactlyGenerated	1
Theorems isProperMap_iff_isCompact_preimage, isProperMap_iff_tendsto_cocompact	2
Total	3

(root)

Definitions

Name	Category	Theorems
CompactlyGenerated 📖	CompData	11 math math: CompactlyGenerated.homeoOfIso_apply, CondensedSet.instIsIsoFunctorCompactlyGeneratedCounitCompactlyGeneratedAdjunction, CompactlyGenerated.compactlyGeneratedToTop_obj, CompactlyGenerated.compactlyGeneratedToTop_map, CompactlyGenerated.isoOfHomeo_hom, CompactlyGenerated.isoOfHomeo_inv, CompactlyGenerated.homeoOfIso_symm_apply, CompactlyGenerated.isoEquivHomeo_symm_apply, CompactlyGenerated.isoEquivHomeo_apply, CompactlyGenerated.instFullTopCatCompactlyGeneratedToTop, CompactlyGenerated.instFaithfulTopCatCompactlyGeneratedToTop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isProperMap_iff_isCompact_preimage 📖	mathematical	—	IsProperMap Continuous IsCompact Set.preimage	—	IsProperMap.continuous IsProperMap.isCompact_preimage isProperMap_iff_isClosedMap_and_compact_fibers CompactlyCoherentSpace.isClosed_iff Set.ext IsClosed.preimage continuous_subtype_val IsCompact.isClosed IsCompact.image IsCompact.inter_left isCompact_singleton
isProperMap_iff_tendsto_cocompact 📖	mathematical	—	IsProperMap Continuous Filter.Tendsto Filter.cocompact	—	Filter.HasBasis.tendsto_right_iff Filter.hasBasis_cocompact IsCompact.compl_mem_cocompact Filter.mem_cocompact IsCompact.of_isClosed_subset IsClosed.preimage IsCompact.isClosed compl_le_compl_iff_le

---

← Back to Index