map_comp

Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

URI: https://scilib.ai/kg/mathlib#PrimeSpectrum.BasicConstructibleSetData.map_comp

← MathLib Explorer

English

The map composition commutes: map (φ ∘ ψ) equals map φ composed with map ψ.

Русский

Композиция отображений сохраняется: map (φ ∘ ψ) = map φ ∘ map ψ.

LaTeX

$$map (φ ∘ ψ) = map φ ∘ map ψ$$

Lean4

theorem map_comp (φ : S →+* T) (ψ : R →+* S) (C : BasicConstructibleSetData R) : C.map (φ.comp ψ) = (C.map ψ).map φ :=
  by simp [map, Function.comp_def]

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

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

Разделы

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

Аффилиация

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