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

∫ Утверждение Mathlib

down_imageHom

Mathlib.Data.Set.Semiring

URI: https://scilib.ai/kg/mathlib#SetSemiring.down_imageHom

← MathLib Explorer

English

The underlying set of imageHom f s is the image under f of the underlying set s.down.

Русский

Опорное множество imageHom f s равно образу f от опорного множества s.down.

LaTeX

$$$(\\mathrm{imageHom}\\ f\\ s)^{\\down} = f '' s^{\\down}$$$

Lean4

@[simp]
theorem down_imageHom [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) :
    (imageHom f s).down = f '' s.down :=
  rfl

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

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

Разделы

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

Аффилиация

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

© 2026 SciLib Lab · ФИЦ ИУ РАН. Все права защищены. Контакты: info@scilibai.ru