range_map

Mathlib.MeasureTheory.Function.SimpleFunc

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.range_map

← MathLib Explorer

English

The range of f.map g is the image of the range of f under g.

Русский

Диапазон f.map g — это образ диапазона f под действием g.

LaTeX

$$$$ \\mathrm{range}(f.map\, g) = \\mathrm{image}(g, \\mathrm{range}(f)). $$$$

Lean4

@[simp]
theorem range_map [DecidableEq γ] (g : β → γ) (f : α →ₛ β) : (f.map g).range = f.range.image g :=
  Finset.coe_injective <| by simp only [coe_range, coe_map, Finset.coe_image, range_comp]

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

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

Разделы

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

Аффилиация

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