Commit 2024-07-12 13:34 12b4bd72

View on Github →

feat(Topology): restriction of a QuotientMap (#13228) ... to the preimage of an open set is a quotient map.

Estimated changes

Modified Mathlib/Data/Set/Function.lean

added theorem Set.image_val_preimage_restrictPreimage

added theorem Set.preimage_restrictPreimage

added theorem Set.restrictPreimage_mk

Modified Mathlib/Topology/Constructions.lean

added theorem QuotientMap.restrictPreimage_isOpen

Modified Mathlib/Topology/ContinuousOn.lean

added theorem QuotientMap.continuousOn_isOpen_iff