not_le_delta

Mathlib.Data.Ordmap.Invariants

URI: https://scilib.ai/kg/mathlib#Ordnode.not_le_delta

English

If s ≥ 1, then s is not ≤ delta·0; in particular s > 0.

Русский

Если s ≥ 1, то s не удовлетворяет s ≤ delta·0; следовательно, s > 0.

LaTeX

$$$1 \\le s \\Rightarrow \\neg (s \\le \\delta \\cdot 0)$$$

Lean4

theorem not_le_delta {s} (H : 1 ≤ s) : ¬s ≤ delta * 0 :=
  not_le_of_gt H

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

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

Разделы

Аффилиация

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