exists_lt_of_directed_le

Mathlib.Order.Directed

URI: https://scilib.ai/kg/mathlib#exists_lt_of_directed_le

English

In a directed poset with ≤, there exist a,b with a < b.

Русский

В направленном множестве с отношением ≤ существуют элементы a,b такие что a < b.

LaTeX

$$$\exists a,b \in \beta: a < b$$$

Lean4

theorem exists_lt_of_directed_le [IsDirected β (· ≤ ·)] : ∃ a b : β, a < b :=
  let ⟨a, b, h⟩ := exists_lt_of_directed_ge βᵒᵈ
  ⟨b, a, h⟩

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

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

Разделы

Аффилиация

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