eq_of_eqOn_dense — Mathlib

English

If two L-Homs agree on a dense set whose closure is the top, then they are equal.

Русский

Если два гомоморфизма по языку L совпадают на плотном множестве, чье замыкание даёт верх, то они равны.

LaTeX

$$$\\text{closure } L\\ s = \\top \\Rightarrow (\\text{EqOn} f g s) \\Rightarrow f = g$$$

Lean4

theorem eq_of_eqOn_dense (hs : closure L s = ⊤) {f g : M →[L] N} (h : s.EqOn f g) : f = g :=
  eq_of_eqOn_top <| hs ▸ eqOn_closure h

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