refl

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#WCovBy.refl

English

For every a in the underlying set, a is covered by itself: the relation is reflexive.

Русский

Для каждого элемента a справедливо a ⩿ a: отношение рефлексивно.

LaTeX

$$$\\\\forall a, a \\\\mathrel{\\\\trianglelefteq} a.$$$

Lean4

theorem refl (a : α) : a ⩿ a :=
  ⟨le_rfl, fun _ hc => hc.not_gt⟩

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

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

Разделы

Аффилиация

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