English
If f: Y → X is open 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 open.
Русский
Если f: Y → X является открытым отображением и для каждого y выполняется p(f(y)), то отображение y ↦ ⟨f(y), hp(y)⟩ из Y в подтип {x ∈ X : p(x)} является открытым отображением.
LaTeX
$$$\text{IsOpenMap}(f) \,\to\, (\forall y, p(f(y))) \,\Rightarrow \, \text{IsOpenMap}(\lambda y, \langle f(y), p(f(y))\rangle).$$$
Lean4
theorem subtype_mk {f : Y → X} (hf : IsOpenMap f) (hp : ∀ x, p (f x)) : IsOpenMap 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
