adjoin_le_equalizer

Mathlib.Algebra.Star.Subalgebra

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

English

If s is a set on which f and g agree, then the adjoin of s is contained in the equalizer of f and g.

Русский

Если на множестве s f и g согласованы, тогда замыкание по adjoin_s входит в равнитель.

LaTeX

$$$ \\mathrm{adjoin}_R s \\le \\mathrm{equalizer}\; f\\; g $$

Lean4

theorem adjoin_le_equalizer {s : Set A} (h : s.EqOn f g) : adjoin R s ≤ StarAlgHom.equalizer f g :=
  adjoin_le h

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

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

Разделы

Аффилиация

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