subtype_mk — Mathlib

English

If f: Y → X is continuous and p(f(y)) holds for all y, then the map y ↦ ⟨f(y), hp(y)⟩ into the subset {x ∈ X : p(x)} is continuous.

Русский

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

LaTeX

$$$\forall f:Y\to X\; (\text{Continuous } f)\; \to \; (\forall y, p(f(y)) ) \Rightarrow (\lambda y, \langle f(y), p(f(y))\rangle) \text{ is continuous }$$

Lean4

@[continuity, fun_prop]
theorem subtype_mk {f : Y → X} (h : Continuous f) (hp : ∀ x, p (f x)) : Continuous fun x => (⟨f x, hp x⟩ : Subtype p) :=
  continuous_induced_rng.2 h

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