exists_pair_lt

Mathlib.Logic.Nontrivial.Basic

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

← MathLib Explorer

English

Every nontrivial linear order contains two distinct elements x,y with x < y.

Русский

Любой ненулевой линейный порядок содержит два разных элемента x,y с x < y.

LaTeX

$$$\exists x \exists y, x < y$$$

Lean4

theorem exists_pair_lt (α : Type*) [Nontrivial α] [LinearOrder α] : ∃ x y : α, x < y :=
  by
  rcases exists_pair_ne α with ⟨x, y, hxy⟩
  cases lt_or_gt_of_ne hxy <;> exact ⟨_, _, ‹_›⟩

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

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

Разделы

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

Аффилиация

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