instRelHomClass

Mathlib.Order.InitialSeg

URI: https://scilib.ai/kg/mathlib#InitialSeg.instRelHomClass

English

There is a RelHomClass structure on InitialSeg r s, i.e., InitialSeg r s carries the capability to be treated as a relational homomorphism class between r and s.

Русский

InitialSeg r s имеет структуру RelHomClass между отношениями r и s.

LaTeX

$$$\\\\text{RelHomClass}(InitialSeg \\\\ r \\\\ s, r, s).$$$

Lean4

instance : RelHomClass (r ≼i s) r s where map_rel f := f.map_rel_iff.2

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

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

Разделы

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

Аффилиация

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