continuous_restrict_apply — Mathlib

English

For a Finset s of X, the map s.restrict f : s → Z is continuous whenever f : X → Z is continuous.

Русский

Для конечного подмножества s пространства X и непрерывного f: X → Z отображение s.restrict f непрерывно.

LaTeX

$$$\text{Continuous}(f) \Rightarrow \text{Continuous}(s\restriction f)$$$

Lean4

@[continuity, fun_prop]
theorem continuous_restrict_apply (s : Finset X) {f : X → Z} (hf : Continuous f) : Continuous (s.restrict f) :=
  hf.comp continuous_subtype_val

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