English
If a function is constant on s and there is a hypothesis that f equals c on closure(s) from every point in closure(s) where continuous within s holds, then f is constant c on closure(s).
Русский
Если функция константа на s и f(x)=c на closure(s) при некоторых условиях непрерывности внутри s, то она константа на closure(s).
LaTeX
$$$(\forall x, x \in \overline{s} \to ContinuousWithinAt f s x) \land s.EqOn f (fun _ => c) \Rightarrow (closure s).EqOn f (fun _ => c)$$$
Lean4
theorem eqOn_const_closure [TopologicalSpace Y] [T1Space Y] {f : X → Y} {s : Set X} {c : Y}
(h : ∀ x ∈ closure s, ContinuousWithinAt f s x) (ht : s.EqOn f (fun _ ↦ c)) : (closure s).EqOn f (fun _ ↦ c) :=
by
intro x hx
apply ContinuousWithinAt.eq_const_of_mem_closure (h x hx) hx ht
