Mathlib Map

Theorems · Theorem · general topology

Continuous.isProperMap

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} [CompactSpace X]
  [T2Space Y], Continuous f → IsProperMap f

A continuous map from a compact space to a T₂ space is a proper map.

Defined in
Mathlib.Topology.Maps.Proper.Basic
Cited by
1 results in Mathlib
Foundations
Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
TopologicalSpaceTopologicalSpaceCompactSpaceT2Space
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

isClosedEmbedding_cfcₙHom_of_cfcHom · cited by 0isClosedEmbedding_cfcₙHom…TopologicalSpace · cited by 24529TopologicalSpaceFilter.Tendsto · cited by 3814Filter.TendstoContinuous · cited by 2592ContinuousT2Space · cited by 1351T2SpaceCompactSpace · cited by 593CompactSpaceFilter.cofinite · cited by 251Filter.cofiniteIsProperMap · cited by 66IsProperMapContinuous.isClosedMap · cited by 9Continuous.isClosedMapFilter.cocompact_eq_bot · cited by 5Filter.cocompact_eq_botisProperMap_iff_isClosedMap_and_tendsto_cofinite · cited by 1isProperMap_iff_isClosedM…Continuous.isProperMapCITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.