lt_irrefl

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.lt_irrefl

English

No CauSeq is strictly less than itself.

Русский

Никакая CauSeq не является строго меньше самой себя.

LaTeX

$$$\forall f\in \mathrm{CauSeq}(\alpha,\mathrm{abs}),\; \neg (f

Lean4

theorem lt_irrefl {f : CauSeq α abs} : ¬f < f
  | h => not_limZero_of_pos h (by simp [zero_limZero])

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

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

Разделы

Аффилиация

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