refl

Mathlib.CategoryTheory.IsConnected

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Zag.refl

English

For any object X in J, Zag X X holds (reflexivity).

Русский

Для любого X в J выполняется Zag X X (рефлексивность).

LaTeX

$$$\\mathrm{Zag}(X,X)$$$

Lean4

@[refl]
theorem refl (X : J) : Zag X X :=
  Or.inl ⟨𝟙 _⟩

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

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

Разделы

Аффилиация

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