IsClosedRestrict

📁 Source: Mathlib/Topology/IsClosedRestrict.lean

Statistics

Metric	Count
Definitions preimageImageRestrict, reorderRestrictProd	2
Theorems isClosed_image_eval, isClosed_image_restrict, continuous_reorderRestrictProd, image_snd_preimageImageRestrict, reorderRestrictProd_mem_preimage_image_restrict, reorderRestrictProd_of_compl, reorderRestrictProd_of_mem, reorderRestrictProd_restrict_compl, restrict_compl_reorderRestrictProd, isClosedMap_restrict_of_compactSpace	10
Total	12

Homeomorph

Definitions

Name	Category	Theorems
preimageImageRestrict 📖	CompOp	1 math math: Topology.image_snd_preimageImageRestrict

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed_image_eval 📖	mathematical	IsCompact Pi.topologicalSpace	IsClosed Set.image	—	IsCompact.isClosed_image_restrict Set.image_comp Homeomorph.isClosed_image

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed_image_restrict 📖	mathematical	IsCompact Pi.topologicalSpace	IsClosed Set.Elem Set Set.instMembership Set.image Set.restrict	—	Topology.image_snd_preimageImageRestrict isCompact_iff_compactSpace image Pi.continuous_restrict isClosedMap_snd_of_compactSpace Homeomorph.isClosed_image IsClosed.preimage continuous_subtype_val

Topology

Definitions

Name	Category	Theorems
reorderRestrictProd 📖	CompOp	6 math math: reorderRestrictProd_restrict_compl, reorderRestrictProd_mem_preimage_image_restrict, reorderRestrictProd_of_mem, continuous_reorderRestrictProd, reorderRestrictProd_of_compl, restrict_compl_reorderRestrictProd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_reorderRestrictProd 📖	mathematical	—	Continuous Set.Elem Set.image Set.restrict Compl.compl Set Set.instCompl instTopologicalSpaceProd instTopologicalSpaceSubtype Set.instMembership Pi.topologicalSpace reorderRestrictProd	—	continuous_pi Continuous.comp' continuous_apply Continuous.snd continuous_id' Continuous.comp continuous_subtype_val continuous_fst
image_snd_preimageImageRestrict 📖	mathematical	—	Set.image Set.Elem Set.restrict Compl.compl Set Set.instCompl Set.preimage DFunLike.coe Homeomorph instTopologicalSpaceSubtype Set.instMembership Pi.topologicalSpace instTopologicalSpaceProd EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.preimageImageRestrict	—	Set.ext Set.image_congr Set.mem_image_of_mem
reorderRestrictProd_mem_preimage_image_restrict 📖	mathematical	—	Set Set.instMembership Set.preimage Set.restrict Compl.compl Set.instCompl Set.image reorderRestrictProd	—	restrict_compl_reorderRestrictProd
reorderRestrictProd_of_compl 📖	mathematical	—	reorderRestrictProd Set Set.instMembership Compl.compl Set.instCompl Set.image Set.restrict Set.Elem	—	Subtype.prop
reorderRestrictProd_of_mem 📖	mathematical	—	reorderRestrictProd Set Set.instMembership Set.Elem Set.image Set.restrict Compl.compl Set.instCompl	—	Subtype.prop
reorderRestrictProd_restrict_compl 📖	mathematical	—	reorderRestrictProd Set.Elem Set.image Set.restrict Compl.compl Set Set.instCompl Set.instMembership Set.preimage	—	—
restrict_compl_reorderRestrictProd 📖	mathematical	—	Set.restrict Compl.compl Set Set.instCompl reorderRestrictProd Set.instMembership Set.image Set.Elem	—	reorderRestrictProd_of_compl

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosedMap_restrict_of_compactSpace 📖	mathematical	CompactSpace	IsClosedMap Pi.topologicalSpace Set.Elem Set Set.instMembership Set.restrict	—	Set.image_comp isClosedMap_fst_of_compactSpace Pi.compactSpace Homeomorph.isClosed_image

---

← Back to Index