ext_on — Mathlib

English

Let s be dense in Y. If f,g: Y → X are continuous and agree on s, then f = g on all of Y.

Русский

Пусть s плотно в Y. Пусть f,g: Y → X непрерывны и совпадают на s, тогда f = g на всем Y.

LaTeX

$$Dense(s) in Y ∧ Continuous(f) ∧ Continuous(g) ∧ f|_s = g|_s ⇒ f = g$$

Lean4

/-- If two continuous functions are equal on a dense set, then they are equal. -/
theorem ext_on [T2Space X] {s : Set Y} (hs : Dense s) {f g : Y → X} (hf : Continuous f) (hg : Continuous g)
    (h : EqOn f g s) : f = g :=
  funext fun x => h.closure hf hg (hs x)

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