up_image

Mathlib.Data.Set.Semiring

URI: https://scilib.ai/kg/mathlib#Set.up_image

English

The upward transport of the set f''s to a SetSemiring equals the imageHom f s.up.

Русский

Перенос вверх множества f''s равенству ImageHom f s .up.

LaTeX

$$$(f '' s).\\uparrow = \\mathrm{imageHom}\\ f\\ s.\\uparrow$$$

Lean4

@[simp]
theorem _root_.Set.up_image [MulOneClass α] [MulOneClass β] (f : α →* β) (s : Set α) : (f '' s).up = imageHom f s.up :=
  rfl

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

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

Разделы

Аффилиация

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