codRestrict — Mathlib

English

If f is continuous and maps every point into a set s, then the codomain-restricted map s.codRestrict f hs is continuous as a function into s.

Русский

Пусть f: X → Y непрерывно, и для каждого a выполнено f(a) ∈ s; тогда отображение s.codRestrict f hs: X → s непрерывно.

LaTeX

$$$\\forall f:X\\to Y,\\; \\forall s\\subseteq Y,\\; (\\text{Continuous}(f) \\wedge \\forall a, f(a)\\in s) \\Rightarrow \\text{Continuous}\\left(s\\codRestrict f hs\\right).$$$

Lean4

@[continuity, fun_prop]
theorem codRestrict {f : X → Y} {s : Set Y} (hf : Continuous f) (hs : ∀ a, f a ∈ s) : Continuous (s.codRestrict f hs) :=
  hf.subtype_mk hs

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