Hom

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.Hom

Lean4

/-- A relation homomorphism with respect to a given pair of relations `R` and `S` s is a function
`f : α → β` such that `a ~[R] b → f a ~[s] f b`. -/
abbrev Hom :=
  (· ~[R] ·) →r (· ~[S] ·)

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

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

Разделы

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

Аффилиация

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