English
If f: Y → X is closed and hp: ∀x, p(f(x)) holds, then the induced map y ↦ ⟨f(y), hp(y)⟩ from Y to the subtype {x ∈ X : p(x)} is closed.
Русский
Если f: Y → X замкнутое отображение и для каждого y выполняется p(f(y)), то отображение y ↦ ⟨f(y), hp(y)⟩ из Y в подтип {x ∈ X : p(x)} замкнуто.
LaTeX
$$$\text{IsClosedMap}(f) \to (\forall y, p(f(y)) ) \Rightarrow \text{IsClosedMap}(\lambda y, \langle f(y), p(f(y))\rangle).$$$
Lean4
theorem subtype_mk {f : Y → X} (hf : IsClosedMap f) (hp : ∀ x, p (f x)) :
IsClosedMap fun x ↦ (⟨f x, hp x⟩ : Subtype p) := fun u hu ↦
by
convert (hf u hu).preimage continuous_subtype_val
exact Set.ext fun _ ↦ exists_congr fun _ ↦ and_congr_right' Subtype.ext_iff
