map_sup

Mathlib.Algebra.Lie.Ideal

URI: https://scilib.ai/kg/mathlib#LieIdeal.map_sup

English

The mapping distributes over joins: map f (I ⊔ I2) = map f I ⊔ map f I2.

Русский

Отображение распределяется по объединению: map f (I ⊔ I2) = map f I ⊔ map f I2.

LaTeX

$$$\\mathrm{map}\_f(I \\sqcup I_2) = \\mathrm{map}\_f(I) \\sqcup \\mathrm{map}\_f(I_2)$$$

Lean4

@[simp]
theorem map_sup : (I ⊔ I₂).map f = I.map f ⊔ I₂.map f :=
  (gc_map_comap f).l_sup

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

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

Разделы

Аффилиация

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