eq_of_eqOn_dense

Mathlib.Algebra.Group.Subgroup.Ker

URI: https://scilib.ai/kg/mathlib#MonoidHom.eq_of_eqOn_dense

← MathLib Explorer

English

If s is dense in G and f, g agree on s, then f = g.

Русский

Если множество s плотно в G и согласие f и g на s, то f = g.

LaTeX

$$$Closure(s) = \top \Rightarrow (\mathrm{EqOn}(f,g;s) \Rightarrow f = g)$$$

Lean4

@[to_additive]
theorem eq_of_eqOn_dense {s : Set G} (hs : closure s = ⊤) {f g : G →* M} (h : s.EqOn f g) : f = g :=
  eq_of_eqOn_top <| hs ▸ eqOn_closure h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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