Commit 2025-03-28 10:45 4e5eb3f7

View on Github →

feat: the restriction of a closed compact set to a subset of coordinates is closed (#22687) Part of the formalization of Kolmogorov's extension theorem.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/IsClosedRestrict.lean

added def Homeomorph.preimageImageRestrict

added theorem IsClosed.isClosed_image_eval

added theorem IsCompact.isClosed_image_restrict

added theorem Topology.continuous_reorderRestrictProd

added theorem Topology.image_snd_preimageImageRestrict

added theorem Topology.reorderRestrictProd_mem_preimage_image_restrict

added theorem Topology.reorderRestrictProd_of_compl

added theorem Topology.reorderRestrictProd_of_mem

added theorem Topology.reorderRestrictProd_restrict_compl

added theorem Topology.restrict_compl_reorderRestrictProd

added theorem isClosedMap_restrict_of_compactSpace