full_ιOfLE

Mathlib.CategoryTheory.ObjectProperty.FullSubcategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.full_ιOfLE

English

If h: P ≤ P' then ιOfLE(h) is full.

Русский

Если h: P ≤ P', то ιOfLE(h) полна.

LaTeX

$$$\forall h:\Pi.hasLe.le\ P\ P', \; (\iotaOfLE h).Full$$$

Lean4

instance full_ιOfLE (h : P ≤ P') : (ιOfLE h).Full :=
  (fullyFaithfulιOfLE h).full

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

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

Разделы

Аффилиация

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