not_le

Mathlib.Order.Preorder.Chain

URI: https://scilib.ai/kg/mathlib#IsChain.not_le

← MathLib Explorer

English

Not (x ≤ y) is equivalent to y < x in a chain on s.

Русский

Not (x ≤ y) эквивалентно y < x в цепи на s.

LaTeX

$$$ IsChain\\ (\\le)\\ s \\rightarrow x \\in s \\rightarrow y \\in s \\rightarrow \\neg (x \\le y) \\leftrightarrow y < x $$$

Lean4

theorem not_le [Preorder α] (hs : IsChain (· ≤ ·) s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : ¬x ≤ y ↔ y < x :=
  ⟨(hs.lt_of_not_ge hx hy ·), fun h h' ↦ h'.not_gt h⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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