map_sup

Mathlib.RingTheory.NonUnitalSubring.Basic

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

English

The image of a join equals the join of images: map f (s ⊔ t) = map f s ⊔ map f t.

Русский

Образ суммы равен сумме образов: map f (s ⊔ t) = map f s ⊔ map f t.

LaTeX

$$$\\mathrm{map}\; f (s \\sqcup t) = \\mathrm{map}\; f s \\sqcup \\mathrm{map}\; f t$$$

Lean4

theorem map_sup (s t : NonUnitalSubring R) (f : F) : (s ⊔ t).map f = s.map f ⊔ t.map f :=
  (gc_map_comap f).l_sup

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

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

Разделы

Аффилиация

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