Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `IsProperMap`	1
Theorems `isProperMap`, `isProperMap`, `isProperMap_subtypeVal`, `isProperMap`, `clusterPt_of_mapClusterPt`, `comp`, `continuous`, `isClosedMap`, `isClosed_range`, `isCompact_preimage`, `pi_map`, `prodMap`, `restrict`, `toContinuous`, `ultrafilter_le_nhds_of_tendsto`, `universally_closed`, `isProperMap`, `isClosedMap_fst_of_compactSpace`, `isClosedMap_snd_of_compactSpace`, `isProperMap_const`, `isProperMap_const_iff`, `isProperMap_fst_of_compactSpace`, `isProperMap_id`, `isProperMap_iff_clusterPt`, `isProperMap_iff_isClosedMap_and_compact_fibers`, `isProperMap_iff_isClosedMap_and_tendsto_cofinite`, `isProperMap_iff_isClosedMap_of_inj`, `isProperMap_iff_ultrafilter`, `isProperMap_iff_ultrafilter_of_t2`, `isProperMap_of_comp_of_inj`, `isProperMap_of_comp_of_surj`, `isProperMap_of_comp_of_t2`, `isProperMap_of_isClosedMap_of_inj`, `isProperMap_snd_of_compactSpace`	34
Total	35

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isProperMap` 📖	mathematical	`Continuous`	`IsProperMap`	—	`isProperMap_iff_isClosedMap_and_tendsto_cofinite` `T2Space.t1Space` `isClosedMap` `Filter.cocompact_eq_bot`

Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isProperMap` 📖	mathematical	—	`IsProperMap` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`continuous` `injective` `isClosedMap`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isProperMap_subtypeVal` 📖	mathematical	—	`IsProperMap` `Set` `Set.instMembership` `instTopologicalSpaceSubtype`	—	`Topology.IsClosedEmbedding.isProperMap` `isClosedEmbedding_subtypeVal`

IsHomeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isProperMap` 📖	mathematical	`IsHomeomorph`	`IsProperMap`	—	`continuous` `injective` `isClosedMap`

IsProperMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clusterPt_of_mapClusterPt` 📖	mathematical	`IsProperMap`	`ClusterPt`	—	—
`comp` 📖	—	`IsProperMap`	—	—	`Continuous.comp'` `continuous` `clusterPt_of_mapClusterPt` `mapClusterPt_comp`
`continuous` 📖	mathematical	`IsProperMap`	`Continuous`	—	`toContinuous`
`isClosedMap` 📖	mathematical	`IsProperMap`	`IsClosedMap`	—	`isClosedMap_iff_clusterPt` `clusterPt_of_mapClusterPt`
`isClosed_range` 📖	mathematical	`IsProperMap`	`IsClosed` `Set.range`	—	`IsClosedMap.isClosed_range` `isClosedMap`
`isCompact_preimage` 📖	mathematical	`IsProperMap` `IsCompact`	`Set.preimage`	—	`isCompact_iff_ultrafilter_le_nhds` `IsCompact.ultrafilter_le_nhds` `Ultrafilter.coe_map` `Filter.map_le_iff_le_comap` `Filter.comap_principal` `ultrafilter_le_nhds_of_tendsto`
`pi_map` 📖	mathematical	`IsProperMap`	`Pi.topologicalSpace`	—	`continuous_pi` `Continuous.comp` `continuous_apply` `nhds_pi` `Filter.le_pi`
`prodMap` 📖	mathematical	`IsProperMap`	`instTopologicalSpaceProd`	—	`Continuous.prodMap` `nhds_prod_eq` `Filter.le_prod`
`restrict` 📖	mathematical	`IsProperMap`	`Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`comp` `IsClosed.isProperMap_subtypeVal`
`toContinuous` 📖	mathematical	`IsProperMap`	`Continuous`	—	—
`ultrafilter_le_nhds_of_tendsto` 📖	mathematical	`IsProperMap` `Filter.Tendsto` `Ultrafilter.toFilter` `nhds`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	—	`isProperMap_iff_ultrafilter`
`universally_closed` 📖	mathematical	`IsProperMap`	`IsClosedMap` `instTopologicalSpaceProd`	—	`isClosedMap` `prodMap` `isProperMap_id`

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isProperMap` 📖	mathematical	`Topology.IsClosedEmbedding`	`IsProperMap`	—	`continuous` `Topology.IsEmbedding.injective` `toIsEmbedding` `isClosedMap`

(root)

Definitions

Name	Category	Theorems
`IsProperMap` 📖	CompData	37 math math: `isProperMap_iff_tendsto_cocompact`, `properSMul_iff`, `isProperMap_iff_ultrafilter`, `isProperMap_iff_clusterPt`, `isProperMap_iff_ultrafilter_of_t2`, `isProperMap_snd_of_compactSpace`, `Homeomorph.isProperMap`, `isProperMap_iff_universally_closed`, `ProperSMul.isProperMap_smul_pair`, `isProperMap_iff_isCompact_preimage`, `isProperMap_fst_of_compactSpace`, `ProperVAdd.isProperMap_vadd_pair`, `IsHomeomorph.isProperMap`, `Polynomial.isProperMap_eval`, `isProperMap_const`, `isProperMap_iff_isClosedMap_and_tendsto_cofinite`, `isProperMap_of_isClosedMap_of_inj`, `isProperMap_iff_isClosedMap_ultrafilter`, `ProperConstVAdd.isProperMap_vadd`, `ProperConstSMul.isProperMap_smul`, `isProperMap_vadd`, `properVAdd_iff`, `isProperMap_iff_isClosedMap_of_inj`, `isProperMap_smul`, `ProperVAdd.isProperMap_vadd_pair_set`, `isProperMap_dist`, `isProperMap_iff_isClosedMap_filter`, `isProperMap_const_iff`, `Topology.IsClosedEmbedding.isProperMap`, `isProperMap_iff_isClosedMap_and_compact_fibers`, `ProperSMul.isProperMap_smul_pair_set`, `Continuous.isProperMap`, `isProperMap_id`, `IsClosed.isProperMap_subtypeVal`, `properSpace_iff_isProperMap_dist`, `AlgebraicGeometry.Scheme.Hom.isProperMap`, `isProperMap_nndist`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosedMap_fst_of_compactSpace` 📖	mathematical	—	`IsClosedMap` `instTopologicalSpaceProd`	—	`IsProperMap.isClosedMap` `isProperMap_fst_of_compactSpace`
`isClosedMap_snd_of_compactSpace` 📖	mathematical	—	`IsClosedMap` `instTopologicalSpaceProd`	—	`IsProperMap.isClosedMap` `isProperMap_snd_of_compactSpace`
`isProperMap_const` 📖	mathematical	—	`IsProperMap`	—	`isProperMap_const_iff`
`isProperMap_const_iff` 📖	mathematical	—	`IsProperMap` `CompactSpace`	—	`isProperMap_iff_isClosedMap_and_compact_fibers` `Set.preimage_const_of_mem` `continuous_const` `isClosedMap_const` `Set.preimage_const`
`isProperMap_fst_of_compactSpace` 📖	mathematical	—	`IsProperMap` `instTopologicalSpaceProd`	—	`IsProperMap.comp` `Homeomorph.isProperMap` `IsProperMap.prodMap` `isProperMap_id` `isProperMap_const` `T2Space.t1Space` `DiscreteTopology.toT2Space` `instDiscreteTopologyPUnit`
`isProperMap_id` 📖	mathematical	—	`IsProperMap`	—	`IsHomeomorph.isProperMap` `IsHomeomorph.id`
`isProperMap_iff_clusterPt` 📖	mathematical	—	`IsProperMap` `Continuous` `ClusterPt`	—	—
`isProperMap_iff_isClosedMap_and_compact_fibers` 📖	mathematical	—	`IsProperMap` `Continuous` `IsClosedMap` `IsCompact` `Set.preimage` `Set` `Set.instSingletonSet`	—	`IsProperMap.continuous` `IsProperMap.isClosedMap` `IsProperMap.isCompact_preimage` `isCompact_singleton` `isProperMap_iff_clusterPt` `IsClosedMap.mapClusterPt_iff_lift'_closure` `inf_le_right` `clusterPt_lift'_closure_iff` `ClusterPt.mono` `inf_le_left`
`isProperMap_iff_isClosedMap_and_tendsto_cofinite` 📖	mathematical	—	`IsProperMap` `Continuous` `IsClosedMap` `Filter.Tendsto` `Filter.cocompact` `Filter.cofinite`	—	`IsCompact.compl_mem_cocompact` `Filter.mem_cocompact` `IsCompact.of_isClosed_subset` `IsClosed.preimage` `isClosed_singleton` `compl_le_compl_iff_le`
`isProperMap_iff_isClosedMap_of_inj` 📖	mathematical	`Continuous`	`IsProperMap` `IsClosedMap`	—	`IsProperMap.isClosedMap` `isProperMap_iff_isClosedMap_and_compact_fibers` `Set.Subsingleton.isCompact` `Set.Subsingleton.preimage` `Set.subsingleton_singleton`
`isProperMap_iff_ultrafilter` 📖	mathematical	—	`IsProperMap` `Continuous` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Ultrafilter.toFilter` `nhds`	—	`isProperMap_iff_clusterPt` `Filter.tendsto_iff_comap` `LE.le.trans` `inf_le_left` `le_inf` `inf_le_right`
`isProperMap_iff_ultrafilter_of_t2` 📖	mathematical	—	`IsProperMap` `Continuous` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Ultrafilter.toFilter` `nhds`	—	`isProperMap_iff_ultrafilter` `tendsto_nhds_unique` `Ultrafilter.neBot` `Filter.Tendsto.mono_left` `Continuous.tendsto`
`isProperMap_of_comp_of_inj` 📖	—	`Continuous` `IsProperMap`	—	—	`IsProperMap.clusterPt_of_mapClusterPt` `ClusterPt.map` `Continuous.continuousAt` `Filter.tendsto_map`
`isProperMap_of_comp_of_surj` 📖	—	`Continuous` `IsProperMap`	—	—	`IsProperMap.clusterPt_of_mapClusterPt` `mapClusterPt_comp` `Filter.map_comap_of_surjective` `ClusterPt.map` `Continuous.continuousAt` `Filter.tendsto_map`
`isProperMap_of_comp_of_t2` 📖	—	`Continuous` `IsProperMap`	—	—	`isProperMap_iff_ultrafilter_of_t2` `isProperMap_iff_ultrafilter` `Filter.Tendsto.comp` `Continuous.tendsto`
`isProperMap_of_isClosedMap_of_inj` 📖	mathematical	`Continuous` `IsClosedMap`	`IsProperMap`	—	—
`isProperMap_snd_of_compactSpace` 📖	mathematical	—	`IsProperMap` `instTopologicalSpaceProd`	—	`IsProperMap.comp` `Homeomorph.isProperMap` `IsProperMap.prodMap` `isProperMap_const` `T2Space.t1Space` `DiscreteTopology.toT2Space` `instDiscreteTopologyPUnit` `isProperMap_id`

---

← Back to Index