instEmbeddingLike

Mathlib.Order.InitialSeg

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

English

Every InitialSeg structure carries an embedding-like structure, i.e., there is a canonical embedding-like organization on InitialSeg r s.

Русский

Каждой структуре InitialSeg соответствует каноническая структура типа embedding-like.

LaTeX

$$$\\\\text{EmbeddingLike}(InitialSeg \\\\ r \\\\ s).$$$

Lean4

instance : EmbeddingLike (r ≼i s) α β where injective' f := f.inj'

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

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

Разделы

Аффилиация

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