eq_of_eqOn_sdense

Mathlib.Algebra.Ring.Subsemiring.Basic

URI: https://scilib.ai/kg/mathlib#RingHom.eq_of_eqOn_sdense

English

If closure s = ⊤, equality on s extends to equality on all of R.

Русский

Если замыкание s равняет ⊤, равенство на s распространяется на всё R.

LaTeX

$$$\\text{closure}(s)=\\top \\Rightarrow f|_s = g|_s \\Rightarrow f=g$$$

Lean4

theorem eq_of_eqOn_sdense {s : Set R} (hs : closure s = ⊤) {f g : R →+* S} (h : s.EqOn f g) : f = g :=
  eq_of_eqOn_stop <| hs ▸ eqOn_sclosure h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru