ext_of_adjoin_eq_top

Mathlib.Algebra.Star.Subalgebra

URI: https://scilib.ai/kg/mathlib#StarAlgHom.ext_of_adjoin_eq_top

← MathLib Explorer

English

If adjoin_R s = ⊤ and hs: s.EqOn f g, then f = g.

Русский

Если adjoin_R s = ⊤ и hs: s.EqOn f g, то f = g.

LaTeX

$$$ (\\mathrm{adjoin}_R s = \\top) \\to (s.EqOn\\ f\\ g) \\Rightarrow f = g $$$

Lean4

theorem ext_of_adjoin_eq_top {s : Set A} (h : adjoin R s = ⊤) ⦃f g : F⦄ (hs : s.EqOn f g) : f = g :=
  DFunLike.ext f g fun _x => StarAlgHom.adjoin_le_equalizer f g hs <| h.symm ▸ trivial

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

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

Разделы

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

Аффилиация

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