English
If f:X→Y is a quotient map and s⊆Y is open, then the restriction to the preimage s.restrictPreimage f is a quotient map.
Русский
Если f: X→Y — квотируемое отображение, и s открыто, то ограничение на предобраз s.restrictPreimage f является квотируемым отображением.
LaTeX
$$$\\forall X,Y,\\; [\\text{TopologicalSpace } X], [\\text{TopologicalSpace } Y],\\; f:X\\to Y,\\; (\\text{IsQuotientMap } f) \\Rightarrow \\forall s, (IsOpen s) \\Rightarrow \\text{IsQuotientMap}\\left(s.restrictPreimage f\\right).$$$
Lean4
/-- If `f : X → Y` is a quotient map,
then its restriction to the preimage of an open set is a quotient map too. -/
theorem restrictPreimage_isOpen {f : X → Y} (hf : IsQuotientMap f) {s : Set Y} (hs : IsOpen s) :
IsQuotientMap (s.restrictPreimage f) :=
by
refine isQuotientMap_iff.2 ⟨hf.surjective.restrictPreimage _, fun U ↦ ?_⟩
rw [hs.isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen, ← hf.isOpen_preimage,
(hs.preimage hf.continuous).isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen, image_val_preimage_restrictPreimage]
