map_range

Mathlib.RingTheory.NonUnitalSubring.Basic

URI: https://scilib.ai/kg/mathlib#NonUnitalRingHom.map_range

English

Mapping a range by g equals the range of the composition g ∘ f.

Русский

Преобразование диапазона через g эквивалентно диапазону композиции g ∘ f.

LaTeX

$$$f.range.map g = (g \\circ f).range$$$

Lean4

theorem map_range : f.range.map g = (g.comp f).range := by
  simpa only [range_eq_map] using (⊤ : NonUnitalSubring R).map_map g f

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

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

Разделы

Аффилиация

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