English
Let X be a Hausdorff space and Y a topological space. If f,g: Y → X are continuous and agree on a subset s ⊆ Y, then they agree on the closure of s.
Русский
Пусть X — топологическое хаусдорфово пространство, Y — другое топологическое пространство. Пусть f,g: Y → X непрерывны и совпадают на подмножестве s ⊆ Y. Тогда они совпадают на замыкании s.
LaTeX
$$$f|_s = g|_s \\rightarrow f|_{\\overline{s}} = g|_{\\overline{s}}$$$
Lean4
/-- If two continuous maps are equal on `s`, then they are equal on the closure of `s`. See also
`Set.EqOn.of_subset_closure` for a more general version. -/
protected theorem closure [T2Space X] {s : Set Y} {f g : Y → X} (h : EqOn f g s) (hf : Continuous f)
(hg : Continuous g) : EqOn f g (closure s) :=
closure_minimal h (isClosed_eq hf hg)
