subtype_coind — Mathlib

English

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

Русский

Если f: Y → X непрерывна и hp: ∀x, p(f(x)) держится, то отображение y ↦ ⟨f(y), hp(y)⟩ из Y в подтип {x ∈ X : p(x)} непрерывно.

LaTeX

$$$\text{Continuous}(f) \to (\forall y, p(f(y))) \Rightarrow \text{Continuous}(\lambda y, \langle f(y), hp(y)\rangle).$$$

Lean4

@[fun_prop]
theorem subtype_coind {f : Y → X} (hf : Continuous f) (hp : ∀ x, p (f x)) : Continuous (Subtype.coind f hp) :=
  hf.subtype_mk hp

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