map

Mathlib.Order.RelSeries

URI: https://scilib.ai/kg/mathlib#RelSeries.map

Lean4

/-- For two types `α, β` and relation on them `r, s`, if `f : α → β` preserves relation `r`, then an
`r`-series can be pushed out to an `s`-series by
`a₀ -r→ a₁ -r→ ... -r→ aₙ ↦ f a₀ -s→ f a₁ -s→ ... -s→ f aₙ`
-/
@[simps length]
def map (p : RelSeries r) (f : r.Hom s) : RelSeries s
    where
  length := p.length
  toFun := f.1.comp p
  step := (f.2 <| p.step ·)

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

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

Разделы

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

Аффилиация

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