subtype_coind — Mathlib

English

If f: Y → X is open 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 open.

Русский

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

Lean4

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

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