refl

Mathlib.Logic.Relator

URI: https://scilib.ai/kg/mathlib#Relator.RightTotal.refl

English

If r₁₁ a a holds for all a, then RightTotal r₁₁.

Русский

Если для каждого a выполняется r₁₁ a a, то правая полнота r₁₁ сохраняется.

LaTeX

$$$ \\forall a:\\\\alpha, r_{11} a a \\Rightarrow \\operatorname{RightTotal}(r_{11}) $$$

Lean4

protected theorem refl (hr : ∀ a : α, r₁₁ a a) : RightTotal r₁₁ :=
  LeftTotal.refl hr

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

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

Разделы

Аффилиация

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