Theorems · Theorem · general topology
isProperMap_iff_ultrafilter
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsProperMap f ↔
Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Filter.Tendsto f (↑𝒰) (nhds y) → ∃ x, f x = y ∧ ↑𝒰 ≤ nhds xCharacterization of proper maps by ultrafilters.
- Defined in
- Mathlib.Topology.Maps.Proper.Basic
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Filterstatement and proof · cited by 8,121
- nhdsstatement and proof · cited by 5,554
- Filter.Tendstostatement and proof · cited by 3,814
- LE.le.transproof · cited by 3,151
- Continuousstatement and proof · cited by 2,592
- Filter.NeBotproof · cited by 853
- Filter.comapproof · cited by 546
- inf_le_leftproof · cited by 286
- inf_le_rightproof · cited by 238
- Ultrafilterstatement and proof · cited by 193
- Ultrafilter.toFilterstatement and proof · cited by 172
Cited by7
Results whose statement or proof uses this declaration.
- IsProperMap.ultrafilter_le_nhds_of_tendstoproof · cited by 1
- properSMul_iff_continuousSMul_ultrafilter_tendstoproof · cited by 1
- isProperMap_iff_ultrafilter_of_t2proof · cited by 1
- isProperMap_iff_isClosedMap_ultrafilterproof · cited by 1
- properVAdd_iff_continuousVAdd_ultrafilter_tendstoproof · cited by 0
- isProperMap_of_comp_of_t2proof · cited by 0
- isProperMap_iff_isClosedMap_filterproof · cited by 0