range_val

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalSubalgebra.range_val

← MathLib Explorer

English

For a Subalgebra S of A, the range of the subtype map equals S.

Русский

Для подпалгебры S ⊆ A образ отображения подмножества равен S.

LaTeX

$$$\operatorname{range}(\mathrm{subtype} \, S) = S$$$

Lean4

theorem range_val : NonUnitalAlgHom.range (NonUnitalSubalgebraClass.subtype S) = S :=
  ext <| Set.ext_iff.1 <| (NonUnitalAlgHom.coe_range <| NonUnitalSubalgebraClass.subtype S).trans Subtype.range_val

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

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

Разделы

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

Аффилиация

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