subtype_coind — Mathlib

English

If f: Y → X is closed and hp: ∀x, p(f(x)) holds, then the induced map from Y to the subtype {x ∈ X : p(x)} given by y ↦ ⟨f(y), hp(y)⟩ is closed.

Русский

Если f: Y → X замкнутое отображение и hp: ∀x, p(f(x)) выполнено, то отображение 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), hp(y)\rangle).$$$

Lean4

theorem subtype_coind {f : Y → X} (hf : IsClosedMap f) (hp : ∀ x, p (f x)) : IsClosedMap (Subtype.coind f hp) :=
  hf.subtype_mk hp

Похожие утверждения