continuousAt_codRestrict_iff — Mathlib

English

If f is defined on X and t is a subset of Y with f(X) ⊆ t, then the codRestrict map has the same continuity at a point as f itself.

Русский

Если f определена на X и f(X) ⊆ t, то codRestrict f t направляет непрерывность в точке x так же, как и f.

LaTeX

$$$\text{ContinuousAt}(\operatorname{codRestrict} f t, x) \iff \text{ContinuousAt}(f, x).$$$

Lean4

@[simp]
theorem continuousAt_codRestrict_iff {f : X → Y} {t : Set Y} (h1 : ∀ x, f x ∈ t) {x : X} :
    ContinuousAt (codRestrict f t h1) x ↔ ContinuousAt f x :=
  IsInducing.subtypeVal.continuousAt_iff

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