eq_const_of_mem_closure — Mathlib

English

If a function is ContinuousWithinAt on a set and equals a constant on that set, then it equals that constant on the closure of the set.

Русский

Если функция непрерывна внутри множества и принимает константу на этом множестве, то она принимает ту же константу на замыкании множества.

LaTeX

$$$\text{ContinuousWithinAt } f s x \to x \in \overline{s} \to (\forall y \in s, f y = c) \Rightarrow f x = c$$$

Lean4

theorem eq_const_of_mem_closure [TopologicalSpace Y] [T1Space Y] {f : X → Y} {s : Set X} {x : X} {c : Y}
    (h : ContinuousWithinAt f s x) (hx : x ∈ closure s) (ht : ∀ y ∈ s, f y = c) : f x = c :=
  by
  rw [← Set.mem_singleton_iff, ← closure_singleton]
  exact h.mem_closure hx ht

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