English
Let X be a T1 space and Y a topological space. For any finite subset s ⊆ X and any function f: X → Y, f is continuous on s (i.e. ContinuousOn f s).
Русский
Пусть X — пространство с топологией T1, Y — топологическое пространство. Для любого конечного множества s ⊆ X и любой функции f: X → Y функция f непрерывна на s (то есть ContinuousOn f s).
LaTeX
$$$ \\forall X\, Y\, [TopologicalSpace X] [T1Space X] [TopologicalSpace Y], \\forall s \\subseteq X,\\ s \\\\text{finite} \\Rightarrow \\forall f:X \\to Y,\\; \\operatorname{ContinuousOn} f\\; s. $$$
Lean4
theorem continuousOn [T1Space X] [TopologicalSpace Y] {s : Set X} (hs : s.Finite) (f : X → Y) : ContinuousOn f s :=
by
rw [continuousOn_iff_continuous_restrict]
have : Finite s := hs
fun_prop
