to_isRefl

Mathlib.Order.Defs.Unbundled

URI: https://scilib.ai/kg/mathlib#IsTotal.to_isRefl

English

A total relation is reflexive.

Русский

Полное отношение (IsTotal) является рефлексивным.

LaTeX

$$$\\\\forall a, \\\\ r(a,a).$$$

Lean4

instance (priority := 100) to_isRefl (r) [IsTotal α r] : IsRefl α r :=
  ⟨fun a => or_self_iff.1 <| total_of r a a⟩

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

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

Разделы

Аффилиация

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