eq_of_eqOn_denseM — Mathlib

English

If closure s = ⊤ (dense), and f,g agree on s, then f = g on M.

Русский

Если замыкание s равно верхней границе (плотно), и f,g совпадают на s, то f = g на всем M.

LaTeX

$$$\\operatorname{closure}(s) = \\top \\;\\Rightarrow\\; (\\forall f,g:\\, M \\to N)[(\\forall x\\in s, f x = g x) \\Rightarrow f = g]$$$

Lean4

@[to_additive]
theorem eq_of_eqOn_denseM {s : Set M} (hs : closure s = ⊤) {f g : M →* N} (h : s.EqOn f g) : f = g :=
  eq_of_eqOn_topM <| hs ▸ eqOn_closureM h

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