Documentation Verification Report

CocompactMap

📁 Source: Mathlib/Topology/ContinuousMap/CocompactMap.lean

Statistics

Metric	Count
Definitions `CocompactMap`, `comp`, `copy`, `id`, `instFunLike`, `instInhabited`, `toContinuousMap`, `CocompactMapClass`, `instCoeTCCocompactMap`, `toCocompactMap`, `toCocompactMap`	11
Theorems `cocompact_tendsto'`, `coe_comp`, `coe_copy`, `coe_id`, `coe_mk`, `coe_toContinuousMap`, `comp_apply`, `comp_assoc`, `comp_id`, `copy_eq`, `ext`, `ext_iff`, `id_comp`, `instCocompactMapClass`, `isCompact_preimage`, `isCompact_preimage_of_isClosed`, `tendsto_of_forall_preimage`, `cocompact_tendsto`, `toContinuousMapClass`, `toCocompactMap_toFun`	20
Total	31

CocompactMap

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	7 math math: `comp_apply`, `ZeroAtInftyContinuousMap.comp_assoc`, `comp_id`, `comp_assoc`, `coe_comp`, `id_comp`, `CompactlySupportedContinuousMap.comp_assoc`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`id` 📖	CompOp	5 math math: `comp_id`, `coe_id`, `CompactlySupportedContinuousMap.comp_id`, `id_comp`, `ZeroAtInftyContinuousMap.comp_id`
`instFunLike` 📖	CompOp	12 math math: `ZeroAtInftyContinuousMap.coe_comp_to_continuous_fun`, `isCompact_preimage_of_isClosed`, `comp_apply`, `instCocompactMapClass`, `ext_iff`, `coe_id`, `Homeomorph.toCocompactMap_toFun`, `coe_toContinuousMap`, `coe_mk`, `isCompact_preimage`, `CompactlySupportedContinuousMap.coe_comp_to_continuous_fun`, `coe_comp`
`instInhabited` 📖	CompOp	—
`toContinuousMap` 📖	CompOp	2 math math: `cocompact_tendsto'`, `coe_toContinuousMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cocompact_tendsto'` 📖	mathematical	—	`Filter.Tendsto` `ContinuousMap.toFun` `toContinuousMap` `Filter.cocompact`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `CocompactMap` `instFunLike` `comp`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `CocompactMap` `instFunLike`	`copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `CocompactMap` `instFunLike` `id`	—	—
`coe_mk` 📖	mathematical	`Filter.Tendsto` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `Filter.cocompact`	`CocompactMap` `instFunLike`	—	—
`coe_toContinuousMap` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `toContinuousMap` `CocompactMap` `instFunLike`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `CocompactMap` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`copy_eq` 📖	mathematical	`DFunLike.coe` `CocompactMap` `instFunLike`	`copy`	—	`DFunLike.ext'`
`ext` 📖	—	`DFunLike.coe` `CocompactMap` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `CocompactMap` `instFunLike`	—	`ext`
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`instCocompactMapClass` 📖	mathematical	—	`CocompactMapClass` `CocompactMap` `instFunLike`	—	`ContinuousMap.continuous_toFun` `cocompact_tendsto'`
`isCompact_preimage` 📖	mathematical	`IsCompact`	`Set.preimage` `DFunLike.coe` `CocompactMap` `instFunLike`	—	`isCompact_preimage_of_isClosed` `IsCompact.isClosed`
`isCompact_preimage_of_isClosed` 📖	mathematical	`IsCompact`	`Set.preimage` `DFunLike.coe` `CocompactMap` `instFunLike`	—	`Filter.mem_cocompact'` `Set.preimage_image_preimage` `Filter.mem_map` `CocompactMapClass.cocompact_tendsto` `instCocompactMapClass` `Filter.mem_cocompact` `Set.compl_subset_compl` `Set.image_preimage_subset` `IsCompact.of_isClosed_subset` `IsClosed.preimage` `ContinuousMapClass.map_continuous` `CocompactMapClass.toContinuousMapClass` `compl_compl`
`tendsto_of_forall_preimage` 📖	mathematical	`IsCompact` `Set.preimage`	`Filter.Tendsto` `Filter.cocompact`	—	`Filter.mem_cocompact` `Filter.mem_map` `Set.preimage_mono`

CocompactMapClass

Definitions

Name	Category	Theorems
`instCoeTCCocompactMap` 📖	CompOp	—
`toCocompactMap` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cocompact_tendsto` 📖	mathematical	—	`Filter.Tendsto` `DFunLike.coe` `Filter.cocompact`	—	—
`toContinuousMapClass` 📖	mathematical	—	`ContinuousMapClass`	—	—

Homeomorph

Definitions

Name	Category	Theorems
`toCocompactMap` 📖	CompOp	1 math math: `toCocompactMap_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toCocompactMap_toFun` 📖	mathematical	—	`DFunLike.coe` `CocompactMap` `CocompactMap.instFunLike` `toCocompactMap` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	—

(root)

Definitions

Name	Category	Theorems
`CocompactMap` 📖	CompData	12 math math: `ZeroAtInftyContinuousMap.coe_comp_to_continuous_fun`, `CocompactMap.isCompact_preimage_of_isClosed`, `CocompactMap.comp_apply`, `CocompactMap.instCocompactMapClass`, `CocompactMap.ext_iff`, `CocompactMap.coe_id`, `Homeomorph.toCocompactMap_toFun`, `CocompactMap.coe_toContinuousMap`, `CocompactMap.coe_mk`, `CocompactMap.isCompact_preimage`, `CompactlySupportedContinuousMap.coe_comp_to_continuous_fun`, `CocompactMap.coe_comp`
`CocompactMapClass` 📖	CompData	2 math math: `CocompactMap.instCocompactMapClass`, `ContinuousMapClass.toCocompactMapClass_of_norm`

---

← Back to Index