UniversallyClosed

Statistics

Metric	Count
Definitions	0
Theorems `isProperMap_iff_isClosedMap_filter`, `isProperMap_iff_isClosedMap_ultrafilter`, `isProperMap_iff_universally_closed`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`isProperMap_iff_isClosedMap_filter` 📖	mathematical	—	`IsProperMap` `Continuous` `IsClosedMap` `Filter` `instTopologicalSpaceProd` `Filter.instTopologicalSpace`	—	`IsProperMap.continuous` `IsProperMap.universally_closed` `isProperMap_iff_ultrafilter` `isClosed_closure` `IsClosed.mem_of_tendsto` `Ultrafilter.neBot` `Filter.Tendsto.prodMk_nhds` `Filter.tendsto_pure_self` `Filter.Eventually.of_forall` `subset_closure` `Ultrafilter.compl_notMem_iff` `mem_closure_iff_nhds` `prod_mem_nhds` `IsOpen.mem_nhds` `Filter.isOpen_setOf_mem`
`isProperMap_iff_isClosedMap_ultrafilter` 📖	mathematical	—	`IsProperMap` `Continuous` `IsClosedMap` `Ultrafilter` `instTopologicalSpaceProd` `Ultrafilter.topologicalSpace`	—	`IsProperMap.continuous` `IsProperMap.universally_closed` `isProperMap_iff_ultrafilter` `isClosed_closure` `IsClosed.mem_of_tendsto` `Ultrafilter.neBot` `Filter.Tendsto.prodMk_nhds` `Ultrafilter.tendsto_pure_self` `Filter.Eventually.of_forall` `subset_closure` `Ultrafilter.compl_notMem_iff` `mem_closure_iff_nhds` `prod_mem_nhds` `IsOpen.mem_nhds` `ultrafilter_isOpen_basic`
`isProperMap_iff_universally_closed` 📖	mathematical	—	`IsProperMap` `Continuous` `IsClosedMap` `instTopologicalSpaceProd`	—	`IsProperMap.continuous` `IsProperMap.universally_closed` `isProperMap_iff_isClosedMap_ultrafilter`

---