le_ind

Mathlib.CategoryTheory.ObjectProperty.Ind

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.le_ind

English

For any P, we have P ≤ ind(P).

Русский

Для любого P выполняется P ≤ ind(P).

LaTeX

$$$P \leq \mathrm{ind}(P)$$$

Lean4

theorem le_ind : P ≤ ind.{w} P := by
  intro X hX
  exact ⟨PUnit, inferInstance, inferInstance, .self X, by simpa⟩

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

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

Разделы

Аффилиация

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